The Design And Implementation Of An Automated Theorem Prover Used For Pointer Logic

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.