随着计算机技术的不断发展,软件已经融入到人们的日常生活和工作生产中,而随着软件规模和复杂度的不断攀升,软件的质量依旧不尽如人意,由此造成的问题对于安全攸关的领域威胁极大。提高软件的可信度是大势所趋,其中基于演绎推理的形式化验证方法就是主要研究方向之一。本课题组设计并开发了安全C语言验证器,它是一款基于演绎推理的C语言程序验证工具,采用了霍尔逻辑和形状图逻辑。形状系统是安全C语言验证器对于形状图逻辑的实现,用于完成堆指针相关程序语句的演算,并限制程序能够使用的易变数据结构及其相关操作。本工作针对形状系统中存在的不足,实施了一系列改进和扩展。第一,扩展了形状系统的演算操作。通过为节点定位演算扩展角标表达式相关的操作规则,把该演算扩展到适用于带角标的指针访问路径的场合,解决原本指针访问路径抽象表述能力不足的问题。此外,本工作还通过函数调用窗口的概念,细化和实现了形状图逻辑中最复杂的函数调用规则,使得形状系统能支持带函数调用语句的验证。第二,改进了形状图的构造方法。形状图构造方法用于从描述堆指针性质的符号断言构造等价的形状图,以便形状系统能够根据构造得到的形状图对堆指针操作语句进行演算。本工作为该方法引入了内置形状谓词,用以简化和复用部分断言描述,并对不同类型的断言施加明确的操作语义,使得形状系统可以正确还原断言描述的形状图,并发现断言中的错误。此外,本工作还引入了自定义谓词到内置形状谓词的推断方法,以尽可能规避内置形状谓词引入后造成的冗余表述的问题。第三,引入了形状检查方法。形状检查方法用以检查程序使用的易变数据结构是否符合安全C语言的相关限定。为表示检查操作的不同严格程度,本工作为形状检查方法引入不同的形状级别,并通过形状分割、形状分析和形状推断这三个阶段分解由易变数据结构中不同指针域带来的复杂性。另外,本工作还通过实现显式形状检查和隐式形状检查,简化形状检查方法的使用。通过本文工作,扩展后的形状系统可以处理表述能力更强、更为复杂的描述形状图的断言,能够支持含有函数调用的程序的演算,并且能够灵活便捷地完成对于易变数据结构是否符合形状定义的检查,最终使得形状系统的功能和性能得到改善。