skip to main content
research-article

A theorem prover for Boolean BI

Published: 23 January 2013 Publication History

Abstract

While separation logic is acknowledged as an enabling technology for large-scale program verification, most of the existing verification tools use only a fragment of separation logic that excludes separating implication. As the first step towards a verification tool using full separation logic, we develop a nested sequent calculus for Boolean BI (Bunched Implications), the underlying theory of separation logic, as well as a theorem prover based on it. A salient feature of our nested sequent calculus is that its sequent may have not only smaller child sequents but also multiple parent sequents, thus producing a graph structure of sequents instead of a tree structure. Our theorem prover is based on backward search in a refinement of the nested sequent calculus in which weakening and contraction are built into all the inference rules. We explain the details of designing our theorem prover and provide empirical evidence of its practicality.

Supplementary Material

JPG File (r2d1_talk8.jpg)
MP4 File (r2d1_talk8.mp4)

References

[1]
N. Belnap. Display logic. Journal of Philosophical Logic, 11: 375--417, 1982.
[2]
N. Belnap. Linear logic displayed. Notre Dame Journal of Formal Logic, 31: 14--25, 1990.
[3]
J. Berdine, C. Calcagno, and P. W. O'Hearn. A decidable fragment of separation logic. Proc. FSTTCS, pages 97--109, 2004.
[4]
Berdine, Calcagno, and O'Hearn}berdine2005smallfootJ. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. Proc. FMCO, pages 115--137, 2005\natexlaba.
[5]
Berdine, Calcagno, and O'Hearn}berdine2005symbolicJ. Berdine, C. Calcagno, and P. W. O'Hearn. Symbolic execution with separation logic. Proc. APLAS, pages 52--68, 2005\natexlabb.
[6]
J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O'Hearn, T. Wies, and H. Yang. Shape analysis for composite data structures. Proc. CAV, pages 178--192, 2007.
[7]
L. Birkedal, N. Torp-Smith, and J. C. Reynolds. Local reasoning about a copying garbage collector. Proc. POPL, pages 220--231, 2004.
[8]
R. Brochenin, S. Demri, and É. Lozes. On the almighty wand. Proc. CSL, pages 323--338, 2008.
[9]
J. Brotherston. A cut-free proof theory for boolean BI (via display logic). Technical Report DTR09--13, Imperial College London, 2009.
[10]
J. Brotherston. A unified display proof theory for bunched logic. Proc. MFPS, pages 197--211, 2010.
[11]
J. Brotherston and M. Kanovich. Undecidability of propositional separation logic and its neighbours. Proc. LICS, pages 130--139, 2010.
[12]
K. Brünnler. Deep sequent systems for modal logic. Proc. Advances in Modal Logic, pages 107--119, 2006.
[13]
B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. Proc. POPL, pages 247--260, 2008.
[14]
D. Distefano and M. J. Parkinson. jStar: towards practical verification for Java. Proc. OOPSLA, pages 213--226, 2008.
[15]
D. Distefano, P. W. O'Hearn, and H. Yang. A local shape analysis based on separation logic. Proc. TACAS, pages 287--302, 2006.
[16]
K. Donnelly, T. Gibson, N. Krishnaswami, S. Magill, and S. Park. The inverse method for the logic of bunched implications. Proc. LPAR, pages 466--480, 2004.
[17]
D. Galmiche and D. Larchey-Wendling. Expressivity properties of boolean BI through relational models. Proc. FSTTCS, pages 357--368, 2006.
[18]
D. Galmiche and D. Méry. Proof-search and countermodel generation in propositional BI logic. Proc. TACS, pages 263--282, 2001.
[19]
D. Galmiche and D. Méry. Semantic labelled tableaux for propositional BI (without bottom). Journal of Logic and Computation, 13: 70--753, 2003.
[20]
D. Galmiche and D. Méry. Tableaux and resource graphs for separation logic. Journal of Logic and Computation, 20: 189--231, 2010.
[21]
D. Galmiche, D. Méry, and D. J. Pym. The semantics of BI and resource tableaux. Mathematical Structures in Computer Science, 15: 1033--1088, 2005.
[22]
R. Goré, L. Postniece, and A. Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. Proc. Advances in Modal Logic, pages 43--66, 2008.
[23]
R. Goré, L. Postniece, and A. Tiu. Taming displayed tense logics using nested sequents with deep inference. Proc. TABLEAUX, pages 189--204, 2009.
[24]
R. Goré, L. Postniece, and A. Tiu. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Logical Methods in Computer Science, 7: 1--38, 2011.
[25]
S. S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. Proc. POPL, pages 14--26, 2001.
[26]
B. Jacobs, J. Smans, and F. Piessens. VeriFast: Imperative programs as proofs. In Proc. VSTTE, pages 59--68, 2010.
[27]
R. Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53 (1): 119--136, 1994.
[28]
D. Larchey-Wendling and D. Galmiche. Exploring the relation between intuitionistic BI and boolean BI: an unexpected embedding. Mathematical Structures in Computer Science, 19: 435--500, 2009.
[29]
D. Larchey-Wendling and D. Galmiche. The undecidability of boolean BI through phase semantics. Proc. LICS, pages 140--149, 2010.
[30]
S. Magill, J. Berdine, E. M. Clarke, and B. Cook. Arithmetic strengthening for shape analysis. Proc. SAS, pages 419--436, 2007.
[31]
N. Marti, R. Affeldt, and A. Yonezawa. Formal verification of the heap manager of an operating system using separation logic. Proc. ICFEM, pages 400--419, 2006.
[32]
J. A. Navarro Pérez and A. Rybalchenko. Separation logic superposition calculus = heap theorem prover. Proc. PLDI, pages 556--566. ACM, 2011.
[33]
H. H. Nguyen and W.-N. Chin. Enhancing program verification with lemmas. Proc. CAV, pages 355--369, 2008.
[34]
P. W. O'Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5: 215--244, 1999.
[35]
D. J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Pub, 2002.
[36]
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. Proc. LICS, pages 55--74, 2002.
[37]
V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. Proc. CONCUR, pages 256--271, 2007.
[38]
H. Yang. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. Proceedings of the 1st Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management, pages 41--68, 2001.

Cited By

View all
  • (2023)Parallel, Distributed Model Checking of Composite Web Services with Integrated Choreography and OrchestrationMachine Learning and Mechanics Based Soft Computing Applications10.1007/978-981-19-6450-3_8(65-76)Online publication date: 28-Feb-2023
  • (2018)Modular Labelled Sequent Calculi for Abstract Separation LogicsACM Transactions on Computational Logic10.1145/319738319:2(1-35)Online publication date: 28-Apr-2018
  • (2018)Modular Tableaux Calculi for Separation TheoriesFoundations of Software Science and Computation Structures10.1007/978-3-319-89366-2_24(441-458)Online publication date: 14-Apr-2018
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
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: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. Boolean BI
  2. nested sequent calculus
  3. separation logic
  4. theorem prover

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)6
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Parallel, Distributed Model Checking of Composite Web Services with Integrated Choreography and OrchestrationMachine Learning and Mechanics Based Soft Computing Applications10.1007/978-981-19-6450-3_8(65-76)Online publication date: 28-Feb-2023
  • (2018)Modular Labelled Sequent Calculi for Abstract Separation LogicsACM Transactions on Computational Logic10.1145/319738319:2(1-35)Online publication date: 28-Apr-2018
  • (2018)Modular Tableaux Calculi for Separation TheoriesFoundations of Software Science and Computation Structures10.1007/978-3-319-89366-2_24(441-458)Online publication date: 14-Apr-2018
  • (2017)Proof Tactics for Assertions in Separation LogicInteractive Theorem Proving10.1007/978-3-319-66107-0_19(285-303)Online publication date: 2017
  • (2014)The formal strong completeness of partial monoidal Boolean BIJournal of Logic and Computation10.1093/logcom/exu03126:2(605-640)Online publication date: 2-Jun-2014
  • (2014)Looking at Separation Algebras with Boolean BI-eyesAdvanced Information Systems Engineering10.1007/978-3-662-44602-7_25(326-340)Online publication date: 2014
  • (2017)Proof Tactics for Assertions in Separation LogicInteractive Theorem Proving10.1007/978-3-319-66107-0_19(285-303)Online publication date: 2017
  • (2016)Completeness for a First-Order Abstract Separation LogicProgramming Languages and Systems10.1007/978-3-319-47958-3_23(444-463)Online publication date: 9-Oct-2016
  • (2015)A branching-time logic to verify synchronously coupled concurrent systems and its relevance to web-based systemsInternational Journal of Web Engineering and Technology10.1504/IJWET.2015.07395010:4(311-333)Online publication date: 1-Dec-2015
  • (2015)Witnessing the elimination of magic wandsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0372-317:6(757-781)Online publication date: 1-Nov-2015
  • 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