skip to main content
research-article

Separation logic + superposition calculus = heap theorem prover

Published: 04 June 2011 Publication History

Abstract

Program analysis and verification tools crucially depend on the ability to symbolically describe and reason about sets of program behaviors. Separation logic provides a promising foundation for dealing with heap manipulating programs, while the development of practical automated deduction/satisfiability checking tools for separation logic is a challenging problem. In this paper, we present an efficient, sound and complete automated theorem prover for checking validity of entailments between separation logic formulas with list segment predicates. Our theorem prover integrates separation logic inference rules that deal with list segments and a superposition calculus to deal with equality/aliasing between memory locations. The integration follows a modular combination approach that allows one to directly incorporate existing advanced techniques for first-order reasoning with equality, as well as account for additional theories, e.g., linear arithmetic, using extensions of superposition. An experimental evaluation of our entailment prover indicates speedups of several orders of magnitude with respect to the available state-of-the-art tools.

References

[1]
T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of c programs. In PLDI, pages 203--213, 2001.
[2]
C. Barrett and C. Tinelli. CVC3. In CAV, pages 298--302, 2007.
[3]
P. Baumgartner and U. Waldmann. Superposition and model evolution combined. In CADE, pages 17--34, 2009.
[4]
J. Berdine, C. Calcagno, and P. W. O'Hearn. A decidable fragment of separation logic. In FSTTCS, number 3328 in LNCS, pages 97--109, 2004.
[5]
J. Berdine, C. Calcagno, and P. W. O'Hearn. Symbolic execution with separation logic. In APLAS, pages 52--68, 2005.
[6]
J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, 2006.
[7]
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, pages 178--192, 2007.
[8]
B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In PLDI, pages 196--207, 2003.
[9]
C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. C. Rinard. Using first-order theorem provers in the Jahob data structure verification system. In VMCAI, pages 74--88, 2007.
[10]
R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, and R. Sebastiani. The MathSAT 4SMT solver. In CAV, pages 299--303, 2008.
[11]
C. Calcagno, M. Parkinson, and V. Vafeiadis. SmallfootRG. In SAS, pages 233--238, 2007.
[12]
C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. In POPL, pages 289--300, 2009.
[13]
B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. In POPL, pages 247--260, 2008.
[14]
L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.
[15]
L. M. de Moura and N. Bjørner. Tapas theory combinations and practical applications. In FORMATS, 2009.
[16]
D. Distefano and M. Parkinson. jStar: Towards practical verification for Java. In OOPSLA, pages 213--226, 2008.
[17]
D. Distefano, P. W. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS, pages 287--302, 2006.
[18]
R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In APLAS, pages 161--177, 2009.
[19]
B. Dutertre and L. D. Moura. The Yices SMT solver. Technical report, Computer Science Laboratory, SRI International, 2006.
[20]
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI, pages 234--245, 2002.
[21]
D. Gay and A. Aiken. Memory management with explicit regions. In PLDI, pages 313--323, 1998.
[22]
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, pages 58--70, 2002.
[23]
B. Jacobs and F. Piessens. The VeriFast program verifier. Technical Report CW-520, Katholieke Universiteit Leuven, Belgium, 2008.
[24]
K. Korovin and A. Voronkov. Integrating linear arithmetic into superposition calculus. In Computer Science Logic (CSL'07), volume 4646 of Lecture Notes in Computer Science, pages 223--237. Springer, 2007.
[25]
N. Marti and R. Affeldt. A certified verifier for a fragment of separation logic. Computer Software, 25 (3): 135--147, 2008.
[26]
M. Méndez-Lojo and M. V. Hermenegildo. Precise set sharing analysis for Java-style programs. In VMCAI, pages 172--187, 2008.
[27]
A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI, pages 221--231, 2001.
[28]
A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent types for imperative programs. In ICFP, pages 229--240, 2008.
[29]
H. H. Nguyen, V. Kuncak, and W.-N. Chin. Runtime checking for separation logic. In VMCAI, pages 203--217, 2008.
[30]
R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In J. A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 7, pages 371--443. Elsevier, 2001.
[31]
A. Podelski and T. Wies. Boolean heaps. In SAS, pages 268--283, 2005.
[32]
A. Podelski and T. Wies. Counterexample-guided focus. In POPL, pages 249--260, 2010.
[33]
J. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002.
[34]
M. C. Rinard. Integrated reasoning and proof choice point selection in the Jahob system -- mechanisms for program survival. In CADE, pages 1--16, 2009.
[35]
S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24 (3): 217--298, 2002.
[36]
J. Villard, É. Lozes, and C. Calcagno. Tracking heaps that hop with Heap-Hop. In TACAS, pages 275--279, 2010.
[37]
H. Yang. An example of local reasoning in bi pointer logic: the schorr-waite graph marking algorithm. In SPACE workshop, 2001.
[38]
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, pages 385--398, 2008.

Cited By

View all
  • (2025)Generically Automating Separation Logic by Functors, Homomorphisms, and ModulesProceedings of the ACM on Programming Languages10.1145/37049039:POPL(1992-2024)Online publication date: 9-Jan-2025
  • (2023)An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capabilityKnowledge-Based Systems10.1016/j.knosys.2022.110217261:COnline publication date: 15-Feb-2023
  • (2021)Compositional optimizations for CertiCoqProceedings of the ACM on Programming Languages10.1145/34735915:ICFP(1-30)Online publication date: 19-Aug-2021
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 46, Issue 6
PLDI '11
June 2011
652 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1993316
Issue’s Table of Contents
  • cover image ACM Conferences
    PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation
    June 2011
    668 pages
    ISBN:9781450306638
    DOI:10.1145/1993498
    • General Chair:
    • Mary Hall,
    • Program Chair:
    • David Padua
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 June 2011
Published in SIGPLAN Volume 46, Issue 6

Check for updates

Author Tags

  1. separation logic
  2. superposition

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)11
  • Downloads (Last 6 weeks)3
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Generically Automating Separation Logic by Functors, Homomorphisms, and ModulesProceedings of the ACM on Programming Languages10.1145/37049039:POPL(1992-2024)Online publication date: 9-Jan-2025
  • (2023)An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capabilityKnowledge-Based Systems10.1016/j.knosys.2022.110217261:COnline publication date: 15-Feb-2023
  • (2021)Compositional optimizations for CertiCoqProceedings of the ACM on Programming Languages10.1145/34735915:ICFP(1-30)Online publication date: 19-Aug-2021
  • (2021)Compositional Satisfiability Solving in Separation LogicVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_26(578-602)Online publication date: 12-Jan-2021
  • (2019)A Decidable Logic for Tree Data-Structures with MeasurementsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_15(318-341)Online publication date: 11-Jan-2019
  • (2018)Frame Inference for Inductive Entailment Proofs in Separation LogicTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-319-89960-2_3(41-60)Online publication date: 12-Apr-2018
  • (2017)Go with the flow: compositional abstractions for concurrent data structuresProceedings of the ACM on Programming Languages10.1145/31581252:POPL(1-31)Online publication date: 27-Dec-2017
  • (2017)Automated lemma synthesis in symbolic-heap separation logicProceedings of the ACM on Programming Languages10.1145/31580972:POPL(1-29)Online publication date: 27-Dec-2017
  • (2017)Compositional entailment checking for a fragment of separation logicFormal Methods in System Design10.1007/s10703-017-0289-451:3(575-607)Online publication date: 3-Aug-2017
  • (2017)A Decidable Fragment in Separation Logic with Inductive Predicates and ArithmeticComputer Aided Verification10.1007/978-3-319-63390-9_26(495-517)Online publication date: 13-Jul-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media