Verifying properties of well-founded linked lists

We describe a novel method for verifying programs that manipulate
linked lists, based on two new predicates that characterize reachability
of heap cells. These predicates allow reasoning about both
acyclic and cyclic lists uniformly with equal ease. The crucial insight
behind our approach is that a circular list invariably contains
a distinguished head cell that provides a handle on the list. This observation
suggests a programming methodology that requires the
heap of the program at each step to be well-founded, i.e., for any
field f in the program, every sequence u.f, u.f.f, . . . contains at
least one head cell. We believe that our methodology captures the
most common idiom of programming with linked data structures.
We enforce our methodology by automatically instrumenting the
program with updates to two auxiliary variables representing these
predicates and adding assertions in terms of these auxiliary variables.
To prove program properties and the instrumented assertions,
we provide a first-order axiomatization of our two predicates. We
also introduce a novel induction principle made possible by the
well-foundedness of the heap. We use our induction principle to
derive from two basic axioms a small set of additional first-order
axioms that are useful for proving the correctness of several programs.
We have implemented our method in a tool and used it to verify
the correctness of a variety of nontrivial programs manipulating
both acyclic and cyclic singly-linked lists and doubly-linked lists.
We also demonstrate the use of indexed predicate abstraction to
automatically synthesize loop invariants for these examples.