Refinement-Based Program Verification via Three-Valued-Logic Analysis
Alexey Loginov
Recently, Sagiv, Reps, and Wilhelm introduced a powerful
abstract-interpretation framework for program analysis based on
three-valued logic. 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 Sagiv, Reps, and Wilhelm has been implemented in the
TVLA tool. 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.
(Click here to access the thesis:
PDF.)
University of Wisconsin