计算机技术的蓬勃发展,使其已经深入到各个领域,从随处可见的智能电子设备到规模庞大的服务器集群,信息服务已经无处不在。在软件功能不断增强的同时,安全问题也变得尤为重要。形式程序验证是提升软件安全性的一种重要方式,而基于演绎推理的程序验证是其中最严格也是最可靠的一种。它根据特定的程序逻辑,通过形式化的演绎推理,并且使用定理证明器进行证明。但由于循环不变式推导困难、定理证明器能力不足等原因,形式程序验证在工业界刚有初步应用。本课题组基于形状图逻辑开发了一个面向PointerC语言进行验证的原型系统,能够完成五种基本形状的验证。但是原型系统中使用的PointerC语言仅为实验性质的类C语言,不具有实用价值。因此本课题组重新开发了安全C语言验证系统,它面向几乎完整C语言进行验证,并且在程序中使用描述能力较强的安全C的规范语言描述程序的行为性质。验证系统验证的一般流程是：以源程序中函数性质的描述为前提,使用符号断言与形状图共同进行演算,最后利用形状图理论以及自动定理证明器来证明演算过程中生成的验证条件。其中形状图用于描述程序中堆指针相关的性质,其演算规则与逻辑关系证明等由形状系统与形状图逻辑提供。而形状图逻辑在许多方面仍然不够完善,特别是针对二叉树形状设计的规则仍然不够全面,这大大限制了验证系统的验证范围。本文的主要工作就是扩充形状图逻辑并且在安全C语言验证系统中基于形状图逻辑实现形状系统。形状图逻辑的扩充包括三个部分,第一部分是通过增加二叉树形状的变换规则、设计判断循环体类型的判断算法以及修改循环不变形状图推断过程,增强形状系统对二叉树程序的验证能力。第二部分是通过对形状图演算规则的简单修改以及增加部分单链表的变换规则,使形状图逻辑更易于实现,也更加适用于C语言的语义。最后一部分是通过对循环不变形状图的推断流程的改进,以减少循环迭代的次数。安全C语言验证系统中形状系统的实现基于本文扩展的形状图逻辑。形状系统使用形状图存储程序中堆指针之间的关系断言,可以为验证系统提供堆指针别名判断、堆指针性质验证、循环不变形状图自动推断以及报告内存泄漏等功能。本文对形状系统实现部分的介绍,主要包括五个部分。它们分别是形状系统验证流程的简单介绍、使用比较统一并且简单的方式基于形状图变换规则对形状图进行展开和折叠的算法说明、通过将形状图转换为指针序列的方式来证明形状图之间蕴含关系的算法实现、改进后循环不变形状图推断流程在形状系统中的实现以及使用虚拟变量与程序变量的对应关系完成形状图的抽象的过程。