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 prov...

• Type: Conference
• Year: 2006
• Where: POPL
• Authors: Shuvendu K. Lahiri, Shaz Qadeer
• Keywords: Auxiliary Variables, Indexed Predicate Abstraction, Induction Principle, POPL 2006, Programming Languages