ABSTRACT
We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose definitions are formalized via user-defined recursive rules. Traditionally, proving relationships between such properties is limited to the unfold-and-match (U+M) paradigm which employs systematic transformation steps of folding/unfolding the rules. A proof, using U+M, succeeds when we find a sequence of transformations that produces a final formula which is obviously provable by simply matching terms. Our contribution here is the addition of the fundamental principle of induction to this automated process. We first show that some proof obligations that are dynamically generated in the process can be used as induction hypotheses in the future, and then we show how to use these hypotheses in an induction step which generates a new proof obligation aside from those obtained by using the fold/unfold operations. While the adding of induction is an obvious need in general, no automated method has managed to include this in a systematic and general way. The main reason for this is the problem of avoiding circular reasoning. We overcome this with a novel checking condition. In summary, our contribution is a proof method which – beyond U+M – performs automatic formula re-writing by treating previously encountered obligations in each proof path as possible induction hypotheses. In the practical evaluation part of this paper, we show how the commonly used technique of using unproven lemmas can be avoided, using realistic benchmarks. This not only removes the current burden of coming up with the appropriate lemmas, but also significantly boosts up the verification process, since lemma applications, coupled with unfolding, often induce a large search space. In the end, our method can automatically reason about a new class of formulas arising from practical program verification.
- J. Berdine, C. Calcagno, and P. O’Hearn. A decidable fragment of separation logic. In FSTTCS, pages 97—-109, 2004. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. O’Hearn. Symbolic execution with separation logic. In APLAS, pages 52––68, 2005. Google ScholarDigital Library
- N. Bjørner and J. Hendrix. Linear functional fixed-points. In CAV, LNCS 5643, 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, LNCS 5710, pages 178––195. Springer, 2009. Google ScholarDigital Library
- R. S. Boyer and J. S. Moore. A theorem prover for a computational logic. In CADE, 1990. Google ScholarDigital Library
- J. Brotherston and J. Villard. Parametric completeness for separation theories. In POPL, pages 453–464, 2014. Google ScholarDigital Library
- J. Brotherston, D. Distefano, and R. L. Petersen. Automated cyclic entailment proofs in separation logic. In CADE, 2011. Google ScholarDigital Library
- J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In APLAS, pages 350–367, 2012.Google ScholarCross Ref
- 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. In SCP, pages 1006––1036, 2012. Google ScholarDigital Library
- D. H. Chu, J. Jaffar, and M. T. Trinh. Automatic induction proofs of data-structures in imperative programs. Technical report, National University of Singapore, 2015.Google Scholar
- 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, 2009. Google ScholarDigital Library
- P. C. Dillinger, P. Manolios, D. Vroon, and J. S. Moore. ACL2s: “The ACL2 Sedan”. In ICSE, 2007.Google Scholar
- G. Duck, J. Jaffar, and N. Koh. A constraint solver for heaps with separation. In CP, LNCS 8124, 2013.Google Scholar
- R. Iosif, A. Rogalewicz, and J. Simachek. The tree width of separation logic with recursive definitions. In CADE, 2013. 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, pages 41––55, 2011. Google ScholarDigital Library
- J. Jaffar and M. J. Maher. Constraint logic programming: A survey. J. LP, 19/20:503–581, May/July 1994.Google ScholarCross Ref
- J. Jaffar, A. E. Santosa, and R. Voicu. A coinduction rule for entailment of recursively defined properties. In CP, 2008. Google ScholarDigital Library
- S. Lahiri and S. Qadeer. Back to the future: revisiting precise program verification using smt solvers. In POPL, pages 171––182. ACM, 2008. Google ScholarDigital Library
- S. K. Lahiri and S. Qadeer. Verifying properties of well-founded linked lists. In POPL, pages 115–126. ACM, 2006. Google ScholarDigital Library
- K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR, LNCS 6355, pages 348––370. Springer, 2010. Google ScholarDigital Library
- K. R. M. Leino. Automating induction with an smt solver. In VMCAI, 2012. Google ScholarDigital Library
- P. Madhusudan, X. Qiu, and A. Stefanescu. Recursive proofs for inductive tree data-structures. In POPL, pages 611–622. 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, 2008. Google ScholarDigital Library
- P. Navarro and A. Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In PLDI, 2011. Google ScholarDigital Library
- H. H. Nguyen and W. N. Chin. Enhancing program verification with lemmas. In CAV ’08, pages 355–369. Springer-Verlag, 2008. Google ScholarDigital Library
- E. Pek, X. Qiu, and P. Madhusudan. Natural proofs for data structure manipulation in c using separation logic. In PLDI, 2014. Google ScholarDigital Library
- R. Piskac, T. Wies, and D. Zufferey. Automating separation logic using smt. In CAV, 2013. Google ScholarDigital Library
- X. Qiu, P. Garg, A. Stefanescu, and P. Madhusudan. Natural proofs for structure, data, and separation. In PLDI, pages 231–242, 2013. 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, 2007. Google ScholarDigital Library
- Z. Rakamaric, R. Bruttomesso, A. J. Hu, and A. Cimatti. Verifying heap-manipulating programs in an smt framework. In ATVA, 2007. Google ScholarDigital Library
- S. Ranise and C. Zarba. A theory of singly-linked lists and its extensible decision procedure. In SEFM, pages 206––215, 2006. Google ScholarDigital Library
- J. Reynolds. A short course on separation logic. http: //www.cs.cmu.edu/afs/cs.cmu.edu/project/ fox-19/member/jcr/wwwaac2003/aac.html, 2003.Google Scholar
- J. C. Reynolds. Separation logic: A logic for shared mutable data objects. In LICS. IEEE, 2002. Google ScholarDigital Library
- G. Rosu and A. Stefanescu. Checking reachability using matching logic. In OOPSLA ’12, pages 555–574. ACM, 2012. Google ScholarDigital Library
- W. Sonnex, S. Drossopoulou, and S. Eisenbach. Zeno: An automated prover for properties of recursive data structures. In TACAS, 2012. Google ScholarDigital Library
- K. Zee, V. Kuncak, and M. Rinard. Full functional verification of linked data structures. In PLDI, pages 349––361. ACM, 2008. Google ScholarDigital Library
- K. Zee, V. Kuncak, and M. Rinard. An integrated proof language for imperative programs. In PLDI, pages 338—-351. ACM, 2009. Google ScholarDigital Library
Index Terms
- Automatic induction proofs of data-structures in imperative programs
Recommendations
Automatic induction proofs of data-structures in imperative programs
PLDI '15We consider the problem of automated reasoning about dynamically manipulated data structures. Essential properties are encoded as predicates whose definitions are formalized via user-defined recursive rules. Traditionally, proving relationships between ...
Imperative Programs as Proofs via Game Semantics
LICS '11: Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer ScienceGame semantics extends the Curry-Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we ...
Effective interactive proofs for higher-order imperative programs
ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programmingWe present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, ...
Comments