一个用于指针程序验证的自动定理证明器的设计与实现

Design and Implementation of an Automated Theorem Prover Used for Pointer Programs Verification

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.

The increasing demands for high-assurance software make the verification of pointer programs a hot research point. As an extension of Hoare logic,Pointer Logic can be used for accurate pointer analysis of pointer programs. This paper introduces some details in designing and implementing of an automated theorem prover for Pointer Logic,and describes some algorithms. The experimental results show our implementation can fully automatically prove the verification conditions for pointer programs in C-like language and produce machine-checkable proofs. The programs for testing are mainly about singly-linked lists,doubly-linked lists and binary trees.