RefinementBased Program Verification Via ThreeValuedLogic Analysis
Alexey Loginov
2006
Recently, Sagiv, Reps, and Wilhelm introduced a powerful abstractinterpretation framework for program analysis based on threevalued logic [84]. Instantiations of this framework have been used to show a number of interesting properties of programs that manipulate a variety of linked data structures. However, two aspects of the framework represented significant challenges in its usermodel. The work that is reported in this thesis addressed these two shortcomings, developed solutions to them, and carried out experiments to demonstrate their effectiveness. The first aspect is the need to specify the set of instrumentation relations, which define the abstraction used in the analysis. This thesis presents a method that refines an abstraction automatically. Refinement is carried out by introducing new instrumentation relations (defined via logical formulas over core relations, which capture the basic properties of memory configurations). We present two strategies for refining an abstraction. The simpler strategy is effective in many cases. The second strategy uses a previously known machinelearning algorithm in a new way, namely, to learn an appropriate abstraction (by learning defining formulas for additional instrumentation relations). An advantage of our method is that it does not require the use of a theorem prover. The use of learning, in lieu of deductionbased techniques, constitutes a paradigm shift: the abstraction is constructed by observing (and generalizing) properties of memory configurations. The second aspect is the need to specify relationmaintenance formulas, which describe how the effect of statements in the language (expressed using logical formulas that describe changes to corerelation values) can be reflected in the values of instrumentation relations. (These formulas define the abstract transfer functions of the abstract semantics used for analyzing programs.) Manual creation of relationmaintenance formulas is a timeconsuming and errorprone process. This thesis presents an algorithm to generate relationmaintenance formulas completely automatically. The algorithm is based on the principle of finite differencing, and transforms an instrumentation relation's defining formula into a relationmaintenance formula that captures what the instrumentation relation's new value should be. The framework of [84] has been implemented in the TVLA tool [54,93]. We have extended TVLA with automatic abstraction refinement and finite differencing and applied it to a number of programs that manipulate (cyclic and acyclic) singly and doublylinked lists, binary trees, and binarysearch trees. The tool was able to demonstrate a number of interesting properties, such as the partial correctness of the programs. Additionally, this thesis reports on the automated verification of the total correctness (partial correctness and termination) of the DeutschSchorrWaite (DSW) algorithm. DSW is an algorithm for traversing a binary tree without the use of a stack by means of destructive pointer manipulation. Prior approaches to the verification of the algorithm involved semiautomated applications of theorem provers or handwritten proofs. TVLA's abstractinterpretation approach made possible the automatic symbolic exploration of all memory configurations that can arise. With the introduction of a few simple core and instrumentation relations, TVLA was able to establish the partial correctness and termination of DSW.
Download this report (PDF)
Return to tech report index
