max planck institut
informatik

We present 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.