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
- Reynolds, John C.,
Intuitionistic Reasoning about Shared Mutable Data Structure.
Millennial Perspectives in Computer Science,
Palgrave, 2000, pp. 303-321.
- Ishtiaq, Samin and O'Hearn, Peter W.,
BI as an Assertion Language for Mutable Data Structures.
POPL 28, January 2001, pp. 14-26.
- Yang, Hongseok,
An Example of Local Reasoning in BI Pointer Logic:
The Schorr-Waite Graph Marking Algorithm.
SPACE 2001, January 2001, pp. 41-68.
- 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.
- 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.
- Yang, Hongseok and O'Hearn, Peter W.,
A Semantic Basis for Local Reasoning.
FOSSACS 2002, LNCS 2303, pp. 402-416.
- Reynolds, John C.,
Separation Logic: A Logic for Shared Mutable Data Structures.
LICS 17, July 2002.
last updated December 16, 2003