Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures

This paper shows how to harness existing theorem provers for first-orderlogic to automatically verify safety properties of imperative programs thatperform dynamic storage allocation and destructive updating of pointer-valuedstructure 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 aconservative way using first-order formulas--the formulas describe a supersetof the set of program states that would be specified if one had a precise wayto express reachability. These methods are employed for semi-automatic programverification (i.e., using programmer-supplied loop invariants) on programs suchas mark-and-sweep garbage collection and destructive reversal of a singlylinked list. (The mark-and-sweep example has been previously reported as beingbeyond the capabilities of ESC/Java.)