Sciweavers

POPL
2006
ACM

Verifying properties of well-founded linked lists

14 years 3 months ago
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...
Shuvendu K. Lahiri, Shaz Qadeer
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Shuvendu K. Lahiri, Shaz Qadeer
Comments (0)