15-818A4 Separation Logic
John C. Reynolds
Second Half of Spring Semester 2004
Mondays and Wednesdays, 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, recursive procedures, and shared-variable concurrency. 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 and examinations.
The first part of this course will be similar in content to a
short course on separation logic
given last fall in Aarhus, Denmark.
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
Homework Assignments (in Postscript)
Last updated: April 22, 2004