Edgar Pek
Xiaokang Qiu
ABSTRACT
The 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 automated reasoning exploiting recursion, mimicking common patterns found in human proofs. However, these proofs are known to work only for a simple toy language [32].
In this work, we develop a framework called VCDryad that extends the Vcc framework [9] to provide an automated deductive framework against separation logic specifications for C programs based on natural proofs. We develop several new techniques to build this framework, including (a) a novel tool architecture that allows encoding natural proofs at a higher level in order to use the existing Vcc framework (including its intricate memory model, the underlying type-checker, and the SMT-based verification infrastructure), and (b) a synthesis of ghost-code annotations that captures natural proof tactics, in essence forcing Vcc to find natural proofs using primarily decidable theories.
We evaluate our tool extensively, on more than 150 programs, ranging from code manipulating standard data structures, well-known open source library routines (Glib, OpenBSD), Linux kernel routines, customized OS data structures, etc. We show that all these C programs can be fully automatically verified using natural proofs (given pre/post conditions and loop invariants) without any user-provided proof tactics. VCDryad is perhaps the first deductive verification framework for heap-manipulating programs in a real language that can prove such a wide variety of programs automatically.
- 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, pages 364--387, 2006. Google Scholar
Digital Library
- J. Berdine, C. Calcagno, and P. W. O'Hearn. A decidable fragment of separation logic. In FSTTCS, pages 97--109, 2004. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. W. O'Hearn. Symbolic execution with separation logic. In APLAS'05, pages 52--68, 2005. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO'05, pages 115--137, 2006. Google ScholarDigital Library
- D. Beyer. Competition on software verification (sv-comp), 2013. URL http://sv-comp.sosy-lab.org/2014/.Google Scholar
- A. R. Bradley, Z. Manna, and H. B. Sipma. What's decidable about arrays? In VMCAI'06, 2006. 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. Sci. Comput. Program., pages 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, 2011. Google ScholarDigital Library
- E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In TPHOLs'09, pages 23--42, 2009. Google ScholarDigital Library
- E. Cohen, M. Moskal, S. Tobies, and W. Schulte. A precise yet efficient memory model for C. Electron. Notes Theor. Comput. Sci., pages 85--103, 2009. Google ScholarDigital Library
- E. Cohen, W. J. Paul, and S. Schmaltz. Theory of multi core hypervisor verification. In SOFSEM'13, pages 1--27, 2013.Google ScholarCross Ref
- J. Condit, B. Hackett, S. K. Lahiri, and S. Qadeer. Unifying type checking and property checking for low-level code. In POPL'09, pages 302--314, 2009. Google ScholarDigital Library
- B. Cook, C. Haase, J. Ouaknine, M. J. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In CONCUR'11, pages 235--249, 2011. Google ScholarDigital Library
- L. M. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD'09, pages 45--52, 2009.Google ScholarCross Ref
- D. Distefano and M. J. Parkinson J. jStar: Towards practical verification for Java. In OOPSLA '08, pages 213--226, 2008. Google ScholarDigital Library
- C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. In FME '01, pages 500--517, 2001. Google ScholarDigital Library
- Y. Ge and L. M. de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In CAV'09, pages 306--320, 2009. Google ScholarDigital Library
- C. Haase, S. Ishtiaq, J. Ouaknine, and M. J. Parkinson. SeLoger: A tool for graph-based reasoning in separation logic. In CAV'13, pages 790--795, 2013. Google ScholarDigital Library
- R. Iosif, A. Rogalewicz, and J. Simácek. The tree width of separation logic with recursive definitions. In CADE-24, pages 21--38, 2013. Google ScholarDigital Library
- S. Itzhaky, A. Banerjee, N. Immerman, A. Nanevski, and M. Sagiv. Effectively-propositional reasoning about reachability in linked data structures. In CAV, pages 756--772, 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'11, pages 41--55, 2011. Google ScholarDigital Library
- M. Kawaguchi, P. M. Rondon, and R. Jhala. Type-based data structure verification. In PLDI'09, pages 304--315, 2009. Google ScholarDigital Library
- C. Le Goues, K. R. M. Leino, and M. Moskal. The Boogie verification debugger. In SEFM'11, pages 407--414, 2011. Google ScholarDigital Library
- K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR-16, pages 348--370, 2010. Google ScholarDigital Library
- P. Madhusudan, X. Qiu, and A. Stefanescu. Recursive proofs for inductive tree data-structures. In POPL'12, pages 123--136, 2012. 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, 2013. Google ScholarDigital Library
- A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI'01, June 2001. Google ScholarDigital Library
- J. A. Navarro Pérez and A. Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In PLDI'11, PLDI '11, pages 556--566, 2011. Google ScholarDigital Library
- P. W. O'Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL'01, pages 1--19, 2001. Google ScholarDigital Library
- P. Philippaerts, J. T. Mühlberg, W. Penninckx, J. Smans, B. Jacobs, and F. Piessens. Software verification with VeriFast: Industrial case studies. Sci. Comput. Program., 82:77--97, 2014. Google ScholarDigital Library
- R. Piskac, T. Wies, and D. Zufferey. Automating separation logic using smt. In CAV'13, 2013. Google ScholarDigital Library
- X. Qiu, P. Garg, A. Stefanescu, and P. Madhusudan. Natural proofs for structure, data, and separation. In PLDI '13, pages 231--242, 2013. Google ScholarDigital Library
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS'02, pages 55--74, 2002. Google ScholarDigital Library
- P. M. Rondon. Liquid Types. PhD thesis, UCSD, 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, 2010. Google ScholarDigital Library
- P. Suter, A. S. Köksal, and V. Kuncak. Satisfiability modulo recursive programs. In SAS'11, pages 298--315, 2011. 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, 2010. Google ScholarDigital Library
Index Terms
- Natural proofs for data structure manipulation in C using separation logic
Recommendations
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 structure, data, and separation
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe 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