ABSTRACT
We 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 of proofs that are amenable to completely automated reasoning, that provide sound but incomplete procedures, and that capture common reasoning tactics in program verification. We develop a dialect of separation logic over heaps, called Dryad, with recursive definitions that avoids explicit quantification. We develop ways to reason with heaplets using classical logic over the theory of sets, and develop natural proofs for reasoning using proof tactics involving disciplined unfoldings and formula abstractions. Natural proofs are encoded into decidable theories of first-order logic so as to be discharged using SMT solvers.
We also implement the technique and show that a large class of more than 100 correct programs that manipulate data-structures are amenable to full functional correctness using the proposed natural proof method. These programs are drawn from a variety of sources including standard data-structures, the Schorr-Waite algorithm for garbage collection, a large number of low-level C routines from the Glib library and OpenBSD library, the Linux kernel, and routines from a secure verified OS-browser project. Our work is the first that we know of that can handle such a wide range of full functional verification properties of heaps automatically, given pre/post and loop invariant annotations. We believe that this work paves the way for deductive verification technology to be used by programmers who do not (and need not) understand the internals of the underlying logic solvers, significantly increasing their applicability in building reliable systems.
Supplemental Material
Available for Download
The supplementary material consists of a PDF file containing the appendices. The appendices describe the natural proof methodology, presented in Section 6 in the paper, in greater detail.
- I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis of single-parent heaps. In VMCAI'07, volume 4349 of LNCS, pages 91--105. Springer, 2007. 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
- J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO'05, volume 4111 of LNCS, pages 115--137. Springer, 2005. Google ScholarDigital Library
- J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O'Hearn, T. Wies, and H. Yang. Shape analysis for composite data structures. In CAV'07, volume 4590 of LNCS, pages 178--192. Springer, 2007. 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
- M. Botinčan, M. Parkinson, and W. Schulte. Separation logic verification of C programs with an SMT solver. ENTCS, 254:5--23, 2009. Google ScholarDigital Library
- A. Bouajjani, C. Drăgoi, C. Enea, and M. Sighireanu. A logic based framework for reasoning about composite data structures. In CONCUR'09, volume 5710 of LNCS, pages 178--195. Springer, 2009. Google ScholarDigital Library
- A. Bouajjani, C. Drăgoi, C. Enea, and M. Sighireanu. On interprocedural analysis of programs with lists and data. In PLDI'11, pages 578--589. ACM, 2011. Google ScholarDigital Library
- M. Bozga, R. Iosif, and S. Perarnau. Quantitative separation logic and programs with lists. In IJCAR'08, volume 5195 of LNCS, pages 34--49. Springer, 2008. Google ScholarDigital Library
- A. R. Bradley, Z.Manna, and H. B. Sipma. What's decidable about arrays? In VMCAI'06, volume 3855 of LNCS, pages 427--442. Springer, 2006. Google ScholarDigital Library
- B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. In POPL'08, pages 247--260. ACM, 2008. Google ScholarDigital Library
- 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, 77(9):1006--1036, 2012. 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
- E. Cohen,M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M.Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In TPHOLs'09, volume 5674 of LNCS, pages 23--42. Springer, 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
- D. Distefano, P. W. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS'06, volume 3920 of LNCS, pages 287--302. Springer, 2006. Google ScholarDigital Library
- T. Hubert and C. Marché. A case study of C source code verification: the Schorr-Waite algorithm. In SEFM'05, pages 190--199. IEEE-CS, 2005. Google ScholarDigital Library
- B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In NFM'11, volume 6617 of LNCS, pages 41--55. Springer, 2011. Google ScholarDigital Library
- N. Klarlund and A. Møller. MONA. BRICS, Department of Computer Science, Aarhus University, January 2001. Available from http://www.brics.dk/mona/.Google Scholar
- 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
- K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR-16, volume 6355 of LNCS, pages 348--370. Springer, 2010. Google ScholarDigital Library
- A. Loginov, T. W. Reps, and M. Sagiv. Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In SAS'06, volume 4134 of LNCS, pages 261--279. Springer, 2006. 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
- P. Madhusudan, X. Qiu, and A. Stefanescu. Recursive proofs for inductive tree data-structures. In POPL'12, pages 123--136. ACM, 2012. 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
- H. Mai, E. Pek, H. Xue, S. T. King, and P. Madhusudan. Verifying security invariants in ExpressOS. In ASPLOS'13, pages 293--304. ACM, 2013. Google ScholarDigital Library
- G. Nelson. Verifying reachability invariants of linked structures. In POPL'83, pages 38--47. ACM, 1983. Google ScholarDigital Library
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. 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. Rakamarić, 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. Rakamarić, 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
- J. Smans, B. Jacobs, and F. Piessens. Implicit dynamic frames. ACM Trans. Program. Lang. Syst., 34(1):2:1--2:58, 2012. 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
- P. Suter, A. S. Köksal, and V. Kuncak. Satisfiability modulo recursive programs. In SAS'11, volume 6887 of LNCS, pages 298--315. Springer, 2011. Google ScholarDigital Library
- H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. W. O'Hearn. Scalable shape analysis for systems code. In CAV'08, volume 5123 of LNCS, pages 385--398. Springer, 2008. Google ScholarDigital Library
- J. Yang and C. Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In PLDI'10, pages 99--110. 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
- Natural proofs for structure, data, and separation
Recommendations
Natural proofs for data structure manipulation in C using separation logic
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and ImplementationThe natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable ...
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 ...
Natural proofs for data structure manipulation in C using separation logic
PLDI '14The natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable ...
Comments