Font Size: a A A

Methods For Overcoming Two Kinds Of Deficiencies Of Automated Theorem Provers In Program Verification

Posted on:2016-05-08Degree:MasterType:Thesis
Country:ChinaCandidate:X HaoFull Text:PDF
GTID:2308330470957745Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
The computer security issue becomes a serious problem in modern society. It needs people to build high-confidence softwares. Formal verification is one of the reliable methods to build high-confidence softwares, and deductive reasoning is a hotspot research field in recent years.One of the previous projects of our laboratory is to design a formal program verification tool based on deductive reasoning which is a program verification prototype system for PointerC language. It is a source-level program verification tool. It derives the relationship between pointers by shape analysis at first, deductively reasons the source program according to an extended Hoare logic, generates verification conditions and then passes them to the automated theorem prover which generates the proofs.There are two kinds of deficiencies of the automated theorem prover in program verification.First, the automated theorem prover can’t deduce propositions by structural induction.Second, the automated theorem prover can’t reason the relation between quantifiers.Based on the previous work of our laboratory, my work improves the prototype system, and focuses on fixing the insufficient problem of the automated theorem provers in program verification.My work makes the following new contributions:First, this paper designs a new method to use automatic induction for proving the correctness of theorems which are provided by programmers. In order to enhance the expressiveness of the assertion language, the prototype system introduces custom predicates. Most of them are defined recursively. Sometimes programmers need to use the inductive properties of these recursively defined predicates. On the other hand, the automated theorem prover can’t reason these properties during the process of proving verification condition. Therefore programmers need to give some relevant auxiliary theorems to help the automated theorem prover to generate proofs. To guarantee the correctness of theorems, this paper proposes a method to analyze the theorems before deducing them by structural induction, and realized the automation of proving theorems.Second, this paper improves the verification capacity of the prototype system for universal quantifier assertions. Since the automated theorem prover can’t reason the relation between quantifiers, it would fail to prove verification condition when there exist some universal quantifiers in them. This paper also proposes an idea of grouping universal quantifier assertions based on shape graphs, and enable the system to verify the verification conditions containing multiple universal quantifiers based on this idea.My work fixes the insufficient problem of the automated theorem provers in the current prototype system. It guarantees the correctness of predicates and theorems provided by programmers. My work not only makes the verifications of programs with operations on mutable data structures more reliable, but also enables the prototype system to verify those programs which have multiple universal quantifiers in their assertions.
Keywords/Search Tags:Formal Verification, Shape Graph Logic, Structural Induction, AutomatedTheorem Proving, Universal Quantifier
PDF Full Text Request
Related items