A Short Course Separation Logic Fall 2003

John C. Reynolds

Course Description

A short course (seven lectures) on separation logic was given under the auspices of BRICS at the University of Aarhus, in the Fall of 2003.

Separation logic is an extension of Hoare logic for reasoning about programs that use shared mutable data structures. We will survey the current development of this logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, recursive procedures, and shared-variable concurrency. We will also discuss promising future directions.

Course Notes (in Postscript)

Minor corrections have been made to some of these notes since they were passed out in class. This is indicated by a more recent revision date.

Brief Bibliography

  1. Reynolds, John C., Intuitionistic Reasoning about Shared Mutable Data Structure. Millennial Perspectives in Computer Science, Palgrave, 2000, pp. 303-321.
  2. Ishtiaq, Samin and O'Hearn, Peter W., BI as an Assertion Language for Mutable Data Structures. POPL 28, January 2001, pp. 14-26.
  3. Yang, Hongseok, An Example of Local Reasoning in BI Pointer Logic: The Schorr-Waite Graph Marking Algorithm. SPACE 2001, January 2001, pp. 41-68.
  4. O'Hearn, Peter W. and Reynolds, John C. and Yang, Hongseok, Local Reasoning about Programs that Alter Data Structures. CSL 2001, LNCS 2142, pp. 1-19.
  5. Calcagno, Cristiano and Yang, Hongseok and O'Hearn, Peter W., Computability and Complexity Results for a Spatial Assertion Language for Data Structures. FST TCS 2001, LNCS 2245, pp. 108-119.
  6. Yang, Hongseok and O'Hearn, Peter W., A Semantic Basis for Local Reasoning. FOSSACS 2002, LNCS 2303, pp. 402-416.
  7. Reynolds, John C., Separation Logic: A Logic for Shared Mutable Data Structures. LICS 17, July 2002.

last updated December 16, 2003