ABSTRACT
We develop logical mechanisms and procedures to facilitate the verification of full functional properties of inductive tree data-structures using recursion that are sound, incomplete, but terminating. Our contribution rests in a new extension of first-order logic with recursive definitions called Dryad, a syntactical restriction on pre- and post-conditions of recursive imperative programs using Dryad, and a systematic methodology for accurately unfolding the footprint on the heap uncovered by the program that leads to finding simple recursive proofs using formula abstraction and calls to SMT solvers. We evaluate our methodology empirically and show that several complex tree data-structure algorithms can be checked against full functional specifications automatically, given pre- and post-conditions. This results in the first automatic terminating methodology for proving a wide variety of annotated algorithms on tree data-structures correct, including max-heaps, treaps, red-black trees, AVL trees, binomial heaps, and B-trees.
Supplemental Material
- I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis by predicate abstraction. In VMCAI'05, volume 3385 of LNCS, pages 164--180. Springer, 2005. Google ScholarDigital Library
- M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R.M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In FMCO'05, volume 4111 of LNCS, pages 364--387. Springer, 2005. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. W. O'Hearn. A decidable fragment of separation logic. In FSTTCS'04, volume 3328 of LNCS, pages 97--109. Springer, 2004. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P.W. O'Hearn. Symbolic execution with separation logic. In APLAS'05, volume 3780 of LNCS, pages 52--68. Springer, 2005. Google ScholarDigital Library
- N. Bjørner and J. Hendrix. Linear functional fixed-points. In CAV'09, volume 5643 of LNCS, pages 124--139. Springer, 2009. Google ScholarDigital Library
- A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu. A logicbased framework for reasoning about composite data structures. In CONCUR'09, volume 5710 of LNCS, pages 178--195. Springer, 2009. Google ScholarDigital Library
- A. R. Bradley and Z. Manna. The Calculus of Computation. Springer, 2007.Google Scholar
- W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming, in press, 2010. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI'11, pages 234--245. ACM, 2011. Google ScholarDigital Library
- T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms. MIT Press, third edition, 2009. Google ScholarDigital Library
- L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS'08, volume 4963 of LNCS, pages 337--340. Springer, 2008. Google ScholarDigital Library
- INRIA. The coq proof assistant. URL http://coq.inria.fr/.Google Scholar
- V. Kuncak, R. Piskac, and P. Suter. Ordered sets in the calculus of data structures. In CSL'10, volume 6247 of LNCS, pages 34--48. Springer, 2010. Google ScholarDigital Library
- S. Lahiri and S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In POPL'08, pages 171--182. ACM, 2008. Google ScholarDigital Library
- P. Madhusudan and X. Qiu. Efficient decision procedures for heaps using STRAND. In SAS'11, volume 6887 of LNCS, pages 43--59. Springer, 2011. Google ScholarDigital Library
- P. Madhusudan, G. Parlato, and X. Qiu. Decidable logics combining heap structures and data. In POPL'11, pages 611--622. ACM, 2011. Google ScholarDigital Library
- S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay. THOR: A tool for reasoning about shape and arithmetic. In CAV'08, volume 5123 of LNCS, pages 428--432. Springer, 2008. Google ScholarDigital Library
- G. Nelson. Verifying reachability invariants of linked structures. In POPL'83, pages 38--47. ACM, 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, volume 2142 of LNCS, pages 1--19. Springer, 2001. Google ScholarDigital Library
- Z. Rakamaric, J. D. Bingham, and A. J. Hu. An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures. In VMCAI'07, volume 4349 of LNCS, pages 106--121. Springer, 2007. Google ScholarDigital Library
- Z. Rakamaric, R. Bruttomesso, A. J. Hu, and A. Cimatti. Verifying heap-manipulating programs in an SMT framework. In ATVA'07, volume 4762 of LNCS, pages 237--252. Springer, 2007. Google ScholarDigital Library
- S. Ranise and C. Zarba. A theory of singly-linked lists and its extensible decision procedure. In SEFM'06, pages 206--215. IEEE-CS, 2006. Google ScholarDigital Library
- J. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS'02, pages 55--74. IEEE-CS, 2002. Google ScholarDigital Library
- G. Rosu, C. Ellison, and W. Schulte. Matching logic: An alternative to Hoare/Floyd logic. In AMAST'10, volume 6486 of LNCS, pages 142--162. Springer, 2010. Google ScholarDigital Library
- P. Suter, M. Dotta, and V. Kuncak. Decision procedures for algebraic data types with abstractions. In POPL'10, pages 199--210. ACM, 2010. Google ScholarDigital Library
- K. Zee, V. Kuncak, and M. C. Rinard. Full functional verification of linked data structures. In PLDI'08, pages 349--361. ACM, 2008. Google ScholarDigital Library
- K. Zee, V. Kuncak, and M. C. Rinard. An integrated proof language for imperative programs. In PLDI'09, pages 338--351. ACM, 2009. Google ScholarDigital Library
Index Terms
- Recursive proofs for inductive tree data-structures
Recommendations
Decidable logics combining heap structures and data
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe define a new logic, STRAND, that allows reasoning with heap-manipulating programs using deductive verification and SMT solvers. STRAND logic ("STRucture ANd Data" logic) formulas express constraints involving heap structures and the data they contain;...
Recursive proofs for inductive tree data-structures
POPL '12We develop logical mechanisms and procedures to facilitate the verification of full functional properties of inductive tree data-structures using recursion that are sound, incomplete, but terminating. Our contribution rests in a new extension of first-...
Natural proofs for structure, data, and separation
PLDI '13We propose natural proofs for reasoning with programs that manipulate data-structures against specifications that describe the structure of the heap, the data stored within it, and separation and framing of sub-structures. Natural proofs are a subclass ...
Comments