Abstract
We 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; they are defined over a class of pointer-structures R defined using MSO-defined relations over trees, and are of the form ∃→x∀→y (→x,→) x" , where "φ" is a monadic second-order logic (MSO) formulawith additional quantification that combines structural constraints as well as data-constraints, but where the data-constraints are only allowed to refer to "→x" and "→y"
The salient aspects of the logic are: (a) the logic is powerful, allowing existential and universal quantification over the nodes, and complex combinations of data and structural constraints; (b) checking Hoare-triples for linear blocks of statements with pre-conditions and post-conditions expressed as Boolean combinations of existential and universal STRAND formulas reduces to satisfiability of a STRAND formula; (c) there are powerful decidable fragments of STRAND, one semantically defined and one syntactically defined, where the decision procedure works by combining the theory of MSO over trees and the quantifier-free theory of the underlying data-logic. We demonstrate the effectiveness and practicality of the logic by checking verification conditions generated in proving properties of several heap-manipulating programs, using a tool that combines an MSO decision procedure over trees (MONA) with an SMT solver for integer constraints (Z3).
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
- T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI'01, pages 203--213. ACM, 2001. 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
- 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
- E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer, 2001.Google Scholar
- A. Bouajjani, C. Dragoi, 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
- L. M. de Moura and N. Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. In IJCAR'08, volume 5195 of LNCS, pages 410--425. Springer, 2008. 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
- J. Engelfriet. Context-free graph grammars. In Handbook of Formal Languages, volume 3, pages 125--214. Springer, 1997. 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, pages 234--245. ACM, 2002. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In PLDI'05, pages 213--223. ACM, 2005. 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
- N. Klarlund and M. I. Schwartzbach. Graph types. In POPL'93, pages 196--205. ACM, 1993. Google ScholarDigital Library
- V. Kuncak. Modular Data Structure Verification. PhD thesis, Massachusetts Institute of Technology, 2007. 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
- T. Lev-Ami and S. Sagiv. Tvla: A system for implementing static analyses. In SAS'00, volume 1824 of LNCS, pages 280--301. Springer, 2000. 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
- S. McPeak and G. C. Necula. Data structure specifications via local equality axioms. In CAV'05, volume 3576 of LNCS, pages 476--490. Springer, 2005. Google ScholarDigital Library
- A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI'01, pages 221--231. ACM, 2001. Google ScholarDigital Library
- G. Nelson. Verifying reachability invariants of linked structures. In POPL'83, pages 38--47. ACM, 1983. Google ScholarDigital Library
- G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst., 1: 245--257, 1979. 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. Yorsh, T. W. Reps, and S. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In TACAS'04, volume 2988 of LNCS, pages 530--545. Springer, 2004.Google Scholar
- G. Yorsh, A. M. Rabinovich, M. Sagiv, A. Meyer, and A. Bouajjani. A logic of reachable patterns in linked data-structures. In FoSSaCS'06, volume 3921 of LNCS, pages 94--110. Springer, 2006. Google ScholarDigital Library
Index Terms
- Decidable logics combining heap structures and data
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;...
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 ...
Decidable Elementary Modal Logics
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer ScienceIn this paper, the modal logic over classes of structures definable by universal first-order Horn formulas is studied. We show that the satisfiability problems for that logics are decidable, confirming the conjecture from [E. Hemaspaandra and H. Schnoor,...
Comments