Simulating Reachability using First-Order Logic
with Applications to Verification of Linked Data Structures
T. Lev-Ami, N. Immerman, T. Reps, M. Sagiv, S. Srivastava, G. Yorsh
This paper shows how to harness existing theorem provers for
first-order logic to automatically verify safety properties of
imperative programs that perform dynamic storage allocation and
destructive updating of pointer-valued structure fields. One of the
main obstacles is specifying and proving the (absence) of reachability
properties among dynamically allocated cells.
The main technical contributions are methods for simulating reachability in a
conservative way using first-order formulas---the formulas describe a superset
of the set of program states that can actually arise. These methods are
employed for semi-automatic program verification (i.e., using
programmer-supplied loop invariants) on programs such as mark-and-sweep garbage
collection and destructive reversal of a singly linked list. (The
mark-and-sweep example has been previously reported as being beyond the
capabilities of ESC/Java.)
(Click here to access the paper:
PostScript,
PDF,
(c) Springer-Verlag.)