15-818A3 Introduction to Separation Logic
John C. Reynolds
First Half of Spring Semester 2007
University Units: 6 (minicourse)
Mondays and Wednesdays 1:30-2:50 pm Wean Hall 4615A
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, shared-variable concurrency, and
read-only sharing. We will also discuss promising future directions.
PREREQUISITES: Some knowledge of predicate logic and Hoare logic.
TEXTS: Papers and notes to be distributed in class.
METHOD OF EVALUATION: Grading will be based on homework.
For an overview survey of separation logic (in postscript),
NOTICE TO STUDENTS - February 23, 2007
The final homework in the minicourse CS818A3 is Exercises 9 to 11 in the
version of Chapter 4 posted on the web on February 23. It is due on the last
day of class, March 5.
NOTICE TO STUDENTS - February 16, 2007
Copies of the Tex sources for the class notes, and relevant files of macros
are available in the directory (not on the web):
Course Notes (in Postscript)
Minor corrections may have been made to some of these notes since they
were passed out in class. This is indicated by a more recent revision
Last updated February 28, 2007