Abstract
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.
- T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: Exploiting program structure for model checking concurrent software. In CONCUR 04: 15th International Conference on Concurrency Theory, volume 3170 of LNCS, pages 1--15. Springer-Verlag, 2004.]]Google ScholarCross Ref
- I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis by predicate abstraction. In VMCAI 05: Verification, Model checking, and Abstract Interpretation, volume 3385 of LNCS, pages 164--180. Springer-Verlag, 2005.]] Google ScholarDigital Library
- T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation, pages 203--213, 2001.]] Google ScholarDigital Library
- C. Barrett and S. Berezin. CVC Lite: A new implementation of the cooperating validity checker. In Computer Aided Verification (CAV'04), volume 3114 of LNCS, pages 515--518. Springer-Verlag, 2004.]]Google Scholar
- M. Benedikt, Thomas W. Reps, and S. Sagiv. A decidable logic for describing linked data structures. In ESOP 99: European Symposium on Programming, volume 1576 of LNCS, pages 2--19. Springer-Verlag, 1999.]] Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. W. O'Hearn. A decidable fragment of separation logic. In FSTTCS 04: Foundations of Software Technology and Theoretical Computer Science, volume 3328 of LNCS, pages 97--109. Springer-Verlag, 2004.]]Google Scholar
- R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Computer-Aided Verification (CAV'02), volume 2404 of LNCS, pages 78--92, July 2002.]] Google ScholarDigital Library
- D. Dams and K. S. Namjoshi. Shape analysis through predicate abstraction and model checking. In VMCAI 03: Verification, Model checking, and Abstract Interpretation, volume 2575 of LNCS, pages 310--324. Springer-Verlag, 2003.]] Google ScholarDigital Library
- D. L. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Technical report, HPL-2003-148, 2003.]]Google Scholar
- E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.]] Google ScholarDigital Library
- G. Dong and J. Su. Incremental and decremental evaluation of transitive closure by first-order queries. Information and Computation, 120(1):101--106, 1995.]] Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI 02: Programming Language Design and Implementation, pages 234--245. ACM Press, 2002.]] Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL 02: Principles of Programming Languages, pages 191--202. ACM Press, 2002.]] Google ScholarDigital Library
- R. Ghiya and L. J. Hendren. Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C. In POPL 96: Principles of Programming Languages, pages 1--15. ACM Press, 1996.]] Google ScholarDigital Library
- S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In Computer-Aided Verification (CAV '97), volume 1254 of LNCS, pages 72--83. Springer-Verlag, June 1997.]] Google ScholarDigital Library
- B. Hackett and R. Rugina. Region-based shape analysis with tracked locations. In POPL 05: Principles of Programming Languages, pages 310--323. ACM Press, 2005.]] Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL 02: Principles of Programming Languages, pages 58--70. ACM Press, 2002.]] Google ScholarDigital Library
- N. Immerman, A. M. Rabinovich, T. W. Reps, S. Sagiv, and G. Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In CSL 04: Computer Science Logic, volume 3210 of LNCS, pages 160--174. Springer-Verlag, 2004.]]Google Scholar
- S. S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. In POPL 01: Principles of Programming Languages, pages 14--26. ACM Press, 2001.]] Google ScholarDigital Library
- N. Klarlund and M. I. Schwartzbach. Graph types. In POPL 93: Principles of Programming Languages, pages 196--205. ACM Press, 1993.]] Google ScholarDigital Library
- S. K. Lahiri and R. E. Bryant. Constructing quantified invariants via predicate abstraction. In VMCAI 04: Verification, Model Checking and Abstract Interpretation, volume 2937 of LNCS, pages 267--281. Springer-Verlag, 2004.]]Google Scholar
- S. K. Lahiri and R. E. Bryant. Indexed predicate discovery for unbounded system verification. In Computer Aided Verification (CAV'04), volume 3114 of LNCS, pages 135--147. Springer-Verlag, 2004.]]Google Scholar
- S. K. Lahiri and S. Qadeer. Verifying properties of well-founded linked lists. Technical Report MSR-TR-2005-97, Microsoft Research, 2005.]]Google Scholar
- T. Lev-Ami, N. Immerman, T. W. Reps, S. Sagiv, S. Srivastava, and G. Yorsh. Simulating reachability using first-order logic with applications to verification of linked data structures. In CADE 05: Conference on Automated Deduction, volume 3632 of LNCS, pages 99--115. Springer-Verlag, 2005.]] Google ScholarDigital Library
- T. Lev-Ami and S. Sagiv. TVLA: A system for implementing static analyses. In SAS 00: Static Analysis Symposium, volume 1824 of LNCS, pages 280--301. Springer-Verlag, 2000.]] Google ScholarDigital Library
- R. Manevich, E. Yahav, G. Ramalingam, and M. Sagiv. Predicate abstraction and canonical abstraction for singly-linked lists. In VMCAI 05: Verification, Model Checking and Abstract Interpretation, volume 3148 of LNCS, pages 181--198. Springer-Verlag, 2005.]] Google ScholarDigital Library
- S. McPeak and G. C. Necula. Data structure specifications via local equality axioms. In Computer-Aided Verification (CAV '05), volume 3576 of LNCS, pages 476--490. Springer-Verlag, 2005.]] Google ScholarDigital Library
- A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI 01: Programming Language Design and Implementation, pages 221--231, 2001.]] Google ScholarDigital Library
- M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In 38th Design Automation Conference (DAC '01), 2001.]] Google ScholarDigital Library
- G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 2(1):245--257, 1979.]] Google ScholarDigital Library
- G. Nelson and F. F. Yao. Solving reachability constraints for linear lists, 1982. Unpublished manuscript.]]Google Scholar
- G. Nelson. Verifying reachability invariants of linked structures. In POPL 83: Principles of Programming Languages, pages 38--47. ACM Press, 1983.]] Google ScholarDigital Library
- P. W. O'Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL 01: 15th International Workshop on Computer Science Logic, volume 2142 of LNCS, pages 1--19. Springer-Verlag, 2001.]] Google ScholarDigital Library
- P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In POPL 04: Principles of Programming Languages, pages 268--280. ACM Press, 2004.]] Google ScholarDigital Library
- S. Ranise and C. Zarba. A decidable logic for pointer programs manipulating linked lists, 2004. Unpublished manuscript.]]Google Scholar
- T. Reps, M. Sagiv, and A. Loginov. Finite differencing of logical formulas for static analysis. In ESOP 03: European Symposium on Programming, volume 2618 of LNCS, pages 380--398. Springer-Verlag, 2003.]]Google ScholarCross Ref
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS 02: Logic in Computer Science, pages 55--74. IEEE Computer Society Press, 2002.]] Google ScholarDigital Library
- R. Wilhelm S. Sagiv, T. W. Reps. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems (TOPLAS), 20(1):1--50, 1998.]] Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In POPL 99: Principles of Programming Languages, pages 105--118. ACM Press, 1999.]] Google ScholarDigital Library
Index Terms
- Verifying properties of well-founded linked lists
Recommendations
Verifying properties of well-founded linked lists
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe 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 ...
Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm's and Tarski's Theorems
Sturm's theorem is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semi-open interval, not counting multiplicity. A generalization of Sturm's theorem is known as ...
Full functional verification of linked data structures
PLDI '08We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verify ...
Comments