Abstraction Refinement for 3-Valued-Logic Analysis
A. Loginov, T. Reps, and M. Sagiv
This paper concerns the question of how to create abstractions that
are useful for program analysis. It presents a method that refines an
abstraction automatically for analysis problems in which the semantics
of statements and the query of interest are expressed using logical
formulas. Refinement is carried out by introducing new
instrumentation relations (defined via logical formulas over core
relations, which capture the basic properties of memory
configurations). A tool that incorporates the algorithm has been
implemented and applied to several algorithms that manipulate linked
lists and binary-search trees. In all but a few cases, the tool is
able to demonstrate (i) the partial correctness of the algorithms, and
(ii) that the algorithms possess additional properties -- e.g.,
stability or antistability.
(Click here to access the paper:
PostScript,
PDF.)