【作者】 王振明；

【导师】 陈意云；

【作者基本信息】 中国科学技术大学 ， 计算机软件与理论， 2009， 博士

【摘要】 对高可信软件需求的增加使得指针程序的验证成为近十几年的研究热点,自动定理证明作为形式化方法之一,在软件验证和程序分析工具当中发挥着及其重要的作用。然而,自动定理证明本身是一个非常难于解决的问题,尤其是待解决的问题中存在着指针以及涉及到指针的递归定义的谓词的情况下。考虑到以上问题,我们在一个出具证明编译器框架中设计并实现了一个自动定理证明器和一个起辅助作用的证明检查器,来帮助完成指针程序的验证。实验结果证明,我们的实现不但具有创新性而且具有实际可行性。在本文中,我们首先介绍了项目的研究背景和理论基础,然后提出了一种为指针逻辑来设计自动定理证明器的新技术,这项技术主要是基于变换和替代,我们已经在一个被称为APL的工具中实现了该技术。指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析。此外,本文还介绍了APL自动定理证明器的详细设计和实现,描述了一些关键算法,比如指针逻辑决策过程,整型线性算术决策过程,证明检查算法等等。APL定理证明器是完全自动的,并且APL所产生的证明可以被有效的记录和检查。在出具证明编译器PLCC 2中,我们调用了APL自动定理证明器,并对一些具有代表性的程序进行了测试。实验结果表明,APL完全可以自动地证明使用类C语言编写的关于单链表,双链表和二叉树的指针程序。本文的主要特色和贡献为:1.提出了一种为指针逻辑设计自动定理证明器的新方法。该方法是为了解决基于指针信息集合表示的验证条件的证明问题而设计的。在实现时我们使用了替代,变换,指针分析等基本技术,在指针信息集合上完成各种推理和证明。并且我们使用这种方法为指针逻辑实现了一个完全自动的定理证明器。这在已存在的比较流行的定理证明器中是不曾实现过的。2.设计了指针逻辑的断言语言和相应的断言演算。该断言语言能够以简洁易懂的形式描述指针逻辑的最显著的特点,主要使用指针信息集合的形式表示待验证的指针程序在各程序点上的状态。断言语言和断言演算是定理证明器和证明检查器设计和实现的基础。3.设计了一个证明检查算法,并在一个证明检查器中实现了该算法。该算法不同于已有的证明检查算法之处在于,它主要是使用模式匹配的方法对以指针信息集合表示为主的证明进行快速有效的检查,来保证证明的正确性。4.实现了一个用于指针逻辑的自动定理证明器。该实现主要包含指针逻辑和整型线性算术两大理论的决策过程,独创的验证条件检查器,证明生成、保存和检查模块等。可以完全自动地证明出具证明编译器PLCC所产生的关于单链表,双链表和二叉树等程序实例的验证条件。APL自动定理证明器的实现,使得出具证明编译器PLCC 2不再需要依赖交互式证明工具Coq,能证明更多的、规模更大的程序实例,整个工具的功能因此变得更加强大。更多还原

【Abstract】 The increasing demands for high-assurance software make the verification of pointer programs a hot research point over the past few years.Automated theorem proving is a method of the form methods,and it plays an important role in many software verification and program analysis tools.However,automated theorem proving is a difficult problem,particularly in the presence of pointers and recursively defined predicates involving pointers.Taking all the problems mentioned above into account,we have designed and implemented an automated theorem prover and an auxiliary proof checker in the framework of a certifying compiler,the prover and checker are used to help accomplishing the verification of programs.The experimental results shows our implementation not only new but also practical.In this paper,we first introduce the research background and theory foundation of the project.Then we present a new technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic,and we have implemented this technique in a tool called APL.As an extension of Hoare logic, Pointer Logic can be used for accurate pointer analysis of pointer programs. Furthermore,this paper introduces some details in designing and implementing of the APL automated theorem prover for Pointer Logic,and describes some algorithms.For example,the decision procedures for Pointer Logic,the decision procedures for linear integer arithmetic,the proof checking algorithm and so on.The APL theorem prover is fully automated and proofs can be recorded and checked efficiently.We invoked the APL theorem prover in the certifying compiler PLCC and tested some representative programs.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.The main contributions and features of this thesis are:1.It presents a new method for designing automated theorem provers for Pointer Logic.This method is designed for proving the verification conditions using pointer information set as its basic form.When implementing,we used some techniques,such as substitute-ion,transformation and pointer analysis,and accomplish reasoning and proving on the pointer information set.We have implemented an automated theorem prover using this method,and we are the first to do so.2.It designs the assertion language and assertion calculus for Pointer Logic.The assertion language can describe the most distinct characters of the Pointer Logic in a compact and pellucid way.The language use the pointer information set to present the state of the program being verified on each point.The assertion language and the corresponding assertion calculus are the basis for designing and implementing the prover and checker.3.It designs a proof checking algorithm,and has implemented this algorithm in a proof checker.The difference between this algorithm and other existing ones is,it use pattern matching to finish proof checking effciently for the proof using pointer information set as its main form,to assure the correctness of the proof.4.It implements an automated theorem prover for Pointer Logic.The implementaion mainly contains the decision procedure of Pointer Logic,the decision procedure of linear integer arithmetic,a unique verification condition checker,proof generation,proof recording,and proof checking and so on.It can automatically prove the verification conditions generated by the PLCC certifying complier for programs about singly-linked list,doubly-linked list and trees.The implementation of APL theorem prover makes the PLCC no longer need to depend on the proof assistant Coq, and can proof more complicated programs;the capability of the whole tool has been improved.更多还原