15-819A4 Separation Logic
John C. Reynolds
Second Half of Spring Semester 2003
Tuesdays and Thursdays, 1:30-2:50 pm Wean Hall 4601
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, and recursive procedures. We will also discuss promising
PREREQUISITES: 15-819A3 or equivalent, or permission of instructor.
TEXT: Notes and papers will be distributed.
METHOD OF EVALUATION: Grading will be based on homework and final exam.
Class Notes (in Postscript)
Section 9 has been substantial rewritten since the end of the
class. Only minor typographical corrections have been made
to the earlier sections. Portions of these notes describe the
results of research supported by NSF Grant CCR-0204242.
An Introduction to Specification Logic, March 10
Expressions, Commands, and Assertions, revised May 23
Specifications and Inference Rules, revised May 23
Lists, revised May 2
Iterated Separating Conjunction, revised May 23
Trees and Dags, revised May 23
Special Classes of Assertions, revised May 23
Information Hiding and the Hypothetical Frame Rule, revised May 23
Proving the Hypothetical Frame Rule, revised May 23
Homework (in Postscript)
Homework 1, March 20, 2003, due April 3
Homework 2, April 3, 2003, due April 10
Homework 3, April 22, 2003, due April 29
Final Exam (take-home), May 1, 2003, due May 8
- 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 June 3, 2003