Skip to main content
SpringerLink
Log in

Automated Cyclic Entailment Proofs in Separation Logic

  • Conference paper
Automated Deduction – CADE-23 (CADE 2011)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6803))

Included in the following conference series:

Abstract

We present a general automated proof procedure, based upon cyclic proof, for inductive entailments in separation logic. Our procedure has been implemented via a deep embedding of cyclic proofs in the HOL Light theorem prover. Experiments show that our mechanism is able to prove a number of non-trivial entailments involving inductive predicates.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 739–782. North-Holland, Amsterdam (1977)

    Chapter  Google Scholar 

  2. Brotherston, J.: Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh (November 2006)

    Google Scholar 

  3. Brotherston, J.: Formalised inductive reasoning in the logic of bunched implications. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 87–103. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: Proceedings of POPL-35, pp. 101–112. ACM, New York (2008)

    Google Scholar 

  5. Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. In: Proceedings of LICS-25, pp. 137–146. IEEE, New York (2010)

    Google Scholar 

  6. Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. Journal of Logic and Computation (2010)

    Google Scholar 

  7. Bundy, A.: The automation of proof by mathematical induction. In: Handbook of Automated Reasoning, vol. I, ch. 13, pp. 845–911. Elsevier Science, Amsterdam (2001)

    Chapter  Google Scholar 

  8. Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Proceedings of POPL-36, pp. 289–300 (2009)

    Google Scholar 

  9. Calcagno, C., O’Hearn, P., Yang, H.: Local action and abstract separation logic. In: Proceedings of LICS-22, pp. 366–378. IEEE, Los Alamitos (2007)

    Google Scholar 

  10. Evan Chang, B.-Y., Rival, X.: Relational inductive shape analysis. In: POPL 2008, pp. 247–260 (2008)

    Google Scholar 

  11. Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384–401. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Distefano, D., O’Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Distefano, D., Parkinson, M.: jStar: Towards practical verification for Java. In: Proceedings of OOPSLA, pp. 213–226. ACM, New York (2008)

    Google Scholar 

  14. Dixon, L., Fleuriot, J.D.: Higher order rippling in isaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 83–98. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. Harrison, J.: HOL light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Martin-Löf, P.: Haupstatz for the intuitionistic theory of iterated inductive definitions. In: Proc. Second Scandinavian Logic Symposium, pp. 179–216 (1971)

    Google Scholar 

  17. Nguyen, H.H., Chin, W.-N.: Enhancing program verification with lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 355–369. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of 17th LICS (2002)

    Google Scholar 

  20. Tuerk, T.: A formalisation of smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469–484. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Voicu, R., Li, M.: Descente infinie proofs in Coq. In: Proceedings of the 1st Coq Workshop, Technische Universität München (2009)

    Google Scholar 

  22. Wirth, C.-P.: Descente Infinie + Deduction. Logic Journal of the IGPL 12(1), 1–96 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  23. Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computing, Imperial College London, UK

    James Brotherston

  2. Dept. of Computer Science, Queen Mary University of London, UK

    Dino Distefano & Rasmus Lerchedahl Petersen

Authors
  1. James Brotherston
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dino Distefano
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rasmus Lerchedahl Petersen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052-6399, Redmond, WA, USA

    Nikolaj Bjørner

  2. Max-Planck-Institut für Informatik, Campus E 1.4, 66123, Saarbrücken, Germany

    Viorica Sofronie-Stokkermans

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brotherston, J., Distefano, D., Petersen, R.L. (2011). Automated Cyclic Entailment Proofs in Separation Logic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22438-6_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22437-9

  • Online ISBN: 978-3-642-22438-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation