15-818A4 Separation Logic

15-818A4 Separation Logic (6 units) Spring 2004

John C. Reynolds

Second Half of Spring Semester 2004

Mondays and Wednesdays, 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, 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 date.

Introduction, revised March 31

Expressions, Commands, and Assertions, revised March 24

Specifications and Inference Rules, revised March 31

Lists and List Segments, revised April 8

Iterated Separating Conjunction, April 8

Trees and Dags, April 12

Special Classes of Assertions. April 22

Homework Assignments (in Postscript)

Assigned March 24, due March 31

Assigned March 31, due April 7

Assigned April 12, due April 19

Assigned April 21, due April 28

Last updated: April 22, 2004