Learning Abstractions for Verifying Data-Structure Properties
Alexey Loginov, Thomas Reps, and Mooly 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.
We present two strategies for refining an abstraction. The simpler
strategy is effective in many cases. The second strategy uses a
known machine-learning algorithm to learn an appropriate abstraction.
A tool that incorporates the method has been
implemented and applied to several programs that manipulate
linked lists and binary-search trees. In all cases, the
tool is able to demonstrate (i) the partial correctness of the
programs, and (ii) that the programs possess additional
properties -- e.g., stability or antistability.
(Click here to access the paper:
PostScript,
PDF.)
University of Wisconsin