Skip Navigation



Journal of Logic and Computation Advance Access published online on January 8, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exn066
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Galmiche, D.
Right arrow Articles by Méry, D.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2008. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Tableaux and Resource Graphs for Separation Logic

Didier Galmiche and Daniel Méry

LORIA - Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy, France.
E-mail: galmiche{at}loria.fr

Received 31 December 2007.

Separation logic (SL) is often presented as an assertion language for reasoning about mutable data structures. As recent results about verification in SL have mainly been achieved from a model-checking point of view, our aim in this article is to study SL from a complementary proof-theoretic perspective in order to provide results about proof search in SL. We begin our study with a fragment of SL, denoted SLP, where first-order quantifiers, variables and equality are removed. We first define specific structures, called resource graphs, that capture SLP models by considering heaps as resources via a labelling process. We then provide a tableau calculus that allows us to build such resource graphs from which either proofs, or countermodels can be generated. We finally prove soundess, completeness and termination of our tableau calculus before discussing extensions to various fragments of SL (including full SL) and the related decidability issues.

Keywords: Separation logic; theorem proving; tableaux; countermodels



References

  1. Berdine J, Calcagno C, O’Hearn P. A decidable fragment of separation logic. (2004) India, Chennai: Springer. 97–109. 24th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2004, Lecture Notes in Computer Science 3328.
  2. Berdine J, Calcagno C, O’Hearn P. Smallfoot: modular automatic assertion checking with separation logic. In: Formal Methods for Components and Objects 2005, Lecture Notes in Computer Science 4111 (2005) Amsterdam, Netherlands: Springer. 115–137.
  3. Berdine J, Calcagno C, O’Hearn P. Symbolic execution with separation logic. (2005) Tsukuba, Japan: Springer. 52–68. 3rd Asian Symposium on Programming Languages and Systems, APLAS 2005, Lecture Notes in Computer Science 3780.
  4. Biri N, Galmiche D. Models and separation logics for resource trees. Journal of Logic and Computation (2007) 17:687–726.[Abstract/Free Full Text]
  5. Bornat R, Calcagno C, O’Hearn P, Parkinson M. Permission accounting in separation logic. (2005) Long Beach, USA: ACM Press. 259–270. 32nd ACM Symposium on Principles of Programming Languages, POPL 2005.
  6. Brochenin R, Demri S, Lozes É. Reasoning about sequences of memory states. (2007) New York, USA: Springer. 100–114. Symposium on Logical Foundations of Computer Science, LFCS 2007, Lecture Notes in Computer Science 4514.
  7. Brochenin R, Demri S, Lozes É. On the almighty wand. In: 22nd International Workshop on Computer Science logic, CSL 2008, Lecture Notes in Computer Science 5213 (2008) Bertinoro, Italy: Springer.
  8. Calcagno C, Gardner P, Zarfaty U. Context logic and tree update. (2005) Long Beach, USA: ACM Press. 271–282. 32nd ACM Symposium on Principles of Programming Languages, POPL 2005.
  9. Calcagno C, Yang H, O’Hearn P. Computability and complexity results for a spatial assertion language for data structures. (2001) Bangalore, India: Springer. 108–119. 21st Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2001, Lecture Notes in Computer Science 2245.
  10. Cardelli L, Gardner P, Ghelli G. A spatial logic for querying graphs. (2002) Malaga Spain: Springer. 597–610. International Conference onAutomata, Langages and Programming, ICALP 2002, Lecture Notes in Computer Science 2380.
  11. Cardelli L, Ghelli G. TQL: a query language for semi-structured data based on the ambient logic. Mathematical Structures in Computer Science (2004) 14:285–327.[CrossRef][Web of Science]
  12. Cardelli L, Gordon AD. Anytime, anywhere - modal logics for mobile ambients. (2000) Boston, USA: ACM Press. 1–13. 27th ACM Symposium on Principles of Programming Languages, POPL 2000.
  13. Distefano D, O’Hearn P, Yang H. A local shape analysis based on separation logic. In: Tools and Algorithms for Construction and Analysis of Systems, TACAS 2006, Lecture Notes in Computer Science 3920 (2006) Vienna, Austria: Springer. 287–302.
  14. Fitting M. Texts and Monographs in Computer Science. In: First-Order Logic and Automated Theorem Proving (1990) New York: Springer.
  15. Galmiche D, Méry D. Characterizing provability in BI's pointer logic through resource graphs. (2005) Montego Bay, Jamaica: Springer. 459–473. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005, Lecture Notes in Artificial Intelligence 3835.
  16. Galmiche D, Méry D, Pym D. The semantics of BI and Resource Tableaux. Mathematical Structures in Computer Science (2005) 15:1033–1088.[CrossRef][Web of Science]
  17. Ishtiaq S, O’Hearn P. BI as an assertion language for mutable data structures. (2001) London, UK: ACM Press. 14–26. 28th ACM Symposium on Principles of Programming Languages, POPL 2001.
  18. Jenson J, Jorgensen M, Klarkund N, Schwartzback M. Automatic verification of pointer programs using monadic second-order logic. (1997) Las Vegas, USA: ACM Press. 225–236. Conference on Programming Language Design and Implementation, PLDI 1997.
  19. Lozes É. Elimination of spatial connectives in static spatial logics. Theoretical Computer Science (2005) 330:475–499.[CrossRef][Web of Science]
  20. Mehta F, Nipkow T. Proving pointer programs in higher-order logic. (2003) Miami, USA: Springer. 121–135. International Conference on Automated Deduction, CADE-19, Lecture Notes in Computer Science 2741.
  21. O’Hearn P, Pym D. The logic of bunched implications. Bulletin of Symbolic Logic (1999) 5:215–244.[CrossRef][Web of Science]
  22. O’Hearn P, Reynolds J, Yang H. Local reasoning about programs that alter data structures. In: 15th International Workshop on Computer Science Logic, CSL 2001, Lecture Notes in Computer Science 2142 (2001) Paris, France: Springer. 1–19.
  23. Ranise S, Deharbe D. Applying light-weight theorem proving to debugging and verifying pointer programs. Electronic Notes in Theoretical Computer Science (2003) 86.
  24. Reynolds J. Separation logic: a logic for shared mutable data structures. (2002) Copenhagen, Denmark: LICS 2002, IEEE Computer Society. 55–74. IEEE Symposium on Logic in Computer Science.
  25. Weber T. Towards mechanized program verification with separation logic. In: 18th International Workshop on Computer Science Logic, CSL 2004, Lecture Notes in Computer Science 3210 (2004) Wroclaw, Poland: Springer. 250–264.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Galmiche, D.
Right arrow Articles by Méry, D.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?