Skip to main content
SpringerLink
Log in

Separation Logic Tutorial

  • Conference paper
Logic Programming (ICLP 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5366))

Included in the following conference series:

  • 1415 Accesses

Abstract

Separation logic is an extension of Hoare’s logic for reasoning about programs that manipulate pointers. It is based on the separating conjunction P ∗ Q, which asserts that P and Q hold for separate portions of computer memory.

This tutorial on separation logic has three parts.

  1. 1

    Basics. Concentrating on highlights from the early work [1,2,3,4].

  2. 1

    Model Theory. The model theory of separation logic evolved from the general resource models of bunched logic [5,6,7] and includes an account of program dynamics in terms of their interaction with resource [8,9].

  3. 1

    Proof Theory. I will describe those aspects of the proof theory, particularly new entailment questions (frame and anti-frame inference [10,11]), which are important for applications in mechanized program verification.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Millennial Perspectives in Computer Science. Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare, Palgrave, pp. 303–321 (2000)

    Google Scholar 

  2. Isthiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: 28th POPL, pp. 36–49 (2001)

    Google Scholar 

  3. O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55–74 (2002)

    Google Scholar 

  5. O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  6. Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer Academic Publishers, Dordrecht (2002)

    Book  MATH  Google Scholar 

  7. Pym, D., O’Hearn, P., Yang, H.: Possible worlds and resources: the semantics of BI. Theoretical Computer Science 315(1), 257–305 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  8. Yang, H., O’Hearn, P.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

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

    Google Scholar 

  10. Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis. Imperial College DOC Tech. Report 2008/12

    Google Scholar 

  12. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Automatic modular assertion checking with separation logic. In: 4th FMCO, pp. 115–137 (2006)

    Google Scholar 

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

    Chapter  Google Scholar 

  14. Magill, S., Nanevski, A., Clarke, E., Lee, P.: Inferring invariants in Separation Logic for imperative list-processing programs. In: 3rd SPACE Workshop (2006)

    Google Scholar 

  15. Berdine, J., Cook, B., Distefano, D., O’Hearn, P.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386–400. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI 2007 (2007)

    Google Scholar 

  17. Guo, B., Vachharajani, N., August, D.: Shape analysis with inductive recursion synthesis. In: PLDI (2007)

    Google Scholar 

  18. Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T., Yang, H.: Shape analysis of composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Magill, S., Tsai, M.-S., Lee, P., Tsay, Y.-K.: THOR: A tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., Wilhelm, R.: A semantics for procedure local heaps and its abstractions. In: 32nd POPL, pp. 296–309 (2005)

    Google Scholar 

  21. Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 240–260. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  24. Distefano, D., Parkinson, M.: jStar: Towards Practical Verification for Java. In: OOPSLA (2008)

    Google Scholar 

  25. Marti, N., Affeldt, R., Yonezawa, A.: Verification of the heap manager of an operating system using separation logic. In: 3rd SPACE Workshop (2006)

    Google Scholar 

  26. Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: 34th POPL, pp. 97–108 (2007)

    Google Scholar 

  27. Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  28. Gardner, P., Smith, G., Wheelhouse, M., Zarfaty, U.: Local Hoare reasoning about DOM. In: 27th PODS, pp. 261–270 (2008)

    Google Scholar 

  29. Parkinson, M., Bierman, G.: Separation logic and abstraction. In: 32nd POPL, pp. 59–70 (2005)

    Google Scholar 

  30. O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science (Reynolds Festschrift) 375(1-3), 271–307 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  31. Brookes, S.D.: A semantics of concurrent separation logic. Theoretical Computer Science (Reynolds Festschrift) 375(1-3), 227–270 (2007)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Queen Mary, Univ. of London, UK

    Peter O’Hearn

Authors
  1. Peter O’Hearn
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Clayton School of Information Technology, Monash University, Australia

    Maria Garcia de la Banda

  2. Department of Computer Science, New Mexico State University, NM 88003, Las Cruces, USA

    Enrico Pontelli

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

O’Hearn, P. (2008). Separation Logic Tutorial. In: Garcia de la Banda, M., Pontelli, E. (eds) Logic Programming. ICLP 2008. Lecture Notes in Computer Science, vol 5366. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89982-2_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-89982-2_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-89981-5

  • Online ISBN: 978-3-540-89982-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation