Refinement-Based Program Verification Via Three-Valued-Logic Analysis

Recently, Sagiv, Reps, and Wilhelm introduced a powerful abstract-interpretation framework for program analysis based on three-valued 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 user-model. 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 machine-learning 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 deduction-based 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 relation-maintenance formulas, which describe how the effect of statements in the language (expressed using logical formulas that describe changes to core-relation 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 relation-maintenance formulas is a time-consuming and error-prone process. This thesis presents an algorithm to generate relation-maintenance formulas completely automatically. The algorithm is based on the principle of finite differencing, and transforms an instrumentation relation's defining formula into a relation-maintenance 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 doubly-linked lists, binary trees, and binary-search 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 Deutsch-Schorr-Waite (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 semi-automated applications of theorem provers or hand-written proofs. TVLA's abstract-interpretation 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