一个程序验证器的设计和实现  

An Automatic Program Verifier for PointerC:Design and Implementation

作　　者：张志天[1,2] 李兆鹏[1,2] 陈意云[1,2] 刘刚[1,2] 

机构地区：[1]中国科学技术大学计算机科学技术学院,合肥230026 [2]中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123

出　　处：《计算机研究与发展》2013年第5期1044-1054,共11页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(61170018;61003043)

摘　　要：形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状图提供的信息来支持程序验证的方法.提出一种利用形状图信息来消除访问路径别名,使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法,并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下,易变数据结构上数据性质的描述和验证方法.另外,介绍所设计并实现的基于上述方法的PointerC语言的程序验证器的原型.它不仅能自动验证操作易变数据结构程序的性质,也能自动验证使用一维数组的程序的性质.Formal verification is hot research areas is automatic a major method to improve the program verification based on dependability of software. One of the logical inference. So far there is no product which can be used directly in the industries, and the root of this problem lies in the slow development and difficulties of automated theorem proving. Our approach is based on the observation that program analysis methods can be used in collecting global information to support program verification. We build shape graphs at each program point in the program analysis phase. A method is proposed, which uses regular Hoare logic rules to reason about assignment not dealing with pointers in a C-like programming language. Such rules will be applied after aliasing is eliminated using the information of shape graphs. The soundness of the logic system has been proved. Furthermore, an approach is presented to verify data constraints on mutable data structures without using user-defined predicates. A prototype of our program verifier has been implemented for the PointerC programming language. We have used it in the verification of programs manipulating recursive data structures, such as lists and trees, and programs dealing with one-dimension arrays.

关 键 词：程序验证 HOARE逻辑 形状图逻辑 程序分析 分离逻辑 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]