Title: Verifying Properties of Well-Founded Linked Lists
Shuvendu Lahiri
November 9, 2005
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 {\em 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
{\em well-founded\/}, i.e., for any field $\myt{f}$ in the program, every
sequence $u.\myt{f},u.\myt{f}.\myt{f},\ldots$ 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.
This is a joint work with Shaz Qadeer that appears in POPL'06.