提高程序验证自动化程度的技术

基于逻辑推理的程序验证是提高软件可信程度的一种重要方法。本项目研究促进程序验证方法走向实用的技术和相关理论，重点解决指针类型给程序验证带来的障碍，为指针程序的自动验证设计一种比较全面的解决办法。.该项研究基于下面的思路：（1）程序验证不必孤立地进行，可用程序分析收集的信息来支持程序验证；（2）程序员可通过提供一些对程序分析和程序验证有用的提示，来换取它们替程序员完成一些很有价值的事情；（3）在通过增强编程语言和断言语言的表达能力来拓展程序验证器的能力时，要尽量避免给自动定理证明器带来太多的负担。.本项目的研究基于上面的思路展开，预计主要亮点是：提出一种直接把形状图作为断言的形状图逻辑，提出形状系统概念。.本项目的研究帮助解决程序自动验证的瓶颈问题，促进程序验证的研究和应用的开展。

1．项目背景. 形式验证是提高软件可信程度的重要方法。其中一条途径是演绎推理，它用形式方法对软件进行数学推理。本项目从设计新的编程语言机制来提高合法程序的门槛，以排除部分有逻辑错误的程序；采用程序分析来收集程序信息，用这些信息来支持程序验证等方法来研究安全C语言的自动程序验证。.2．主要研究内容. （1）面向自动程序验证的C语言子集的设计。. （2）在C语言中，面向易变数据结构的形状系统的设计。. （3）用于实现形状系统的形状图逻辑的设计. （4）安全C语言的规范语言SCSL（Safe C Specification Language）的设计. （5）提升程序验证器的证明能力的探索. （6）设计并实现安全C语言的程序验证器.3．重要结果. （1）以禁止无法推断的别名和限制可推断的别名为指导思想，设计了一种面向自动程序验证的安全C语言。. （2）为易于验证操作易变数据结构的程序，设计了面向易变数据结构的形状系统以及相关的形状图逻辑。. （3）定义了形状图的语法理论和语义理论，定义了形状图重写系统及其终止性、局部合流性和合流性，提出了基于形状图重写的形状图等价判定和蕴涵判定的方法。. （4）设计了具有自己特色的、用于书写函数前后条件和循环不变式等的安全C语言的规范语言SCSL。. （5）实现了安全C语言程序验证器的一个初步原型，已经能够自动验证百行左右的操作各类指针或数组的程序。.4．科学意义. 本项目研究促进基于演绎推理的程序验证方法走向实用的技术和相关理论，重点解决了指针类型给程序验证带来的障碍，把程序验证技术推进到能为用安全C语言写的实际程序进行自动验证的阶段。