15-819A4 Separation Logic
(6 units)
Spring 2003
John C. Reynolds
Second Half of Spring Semester 2003
Tuesdays and Thursdays, 1:30-2:50 pm Wean Hall 4601
Course Description
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
future directions.
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.
1.
An Introduction to Specification Logic, March 10
2.
Expressions, Commands, and Assertions, revised May 23
3.
Specifications and Inference Rules, revised May 23
4.
Lists, revised May 2
5.
Iterated Separating Conjunction, revised May 23
6.
Trees and Dags, revised May 23
7.
Special Classes of Assertions, revised May 23
8.
Information Hiding and the Hypothetical Frame Rule, revised May 23
9.
Proving the Hypothetical Frame Rule, revised May 23
Homework (in Postscript)
1.
Homework 1, March 20, 2003, due April 3
2.
Homework 2, April 3, 2003, due April 10
3.
Homework 3, April 22, 2003, due April 29
4.
Final Exam (take-home), May 1, 2003, due May 8
Tentative 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 June 3, 2003