15-818A3 Introduction to Separation Logic

15-818A3 Introduction to Separation Logic (6 units) Spring 2005

John C. Reynolds

First Half of Spring Semester 2005

University Units: 6 (minicourse)

Mondays and Wednesdays, noon-1:50 pm Wean Hall 4615A

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, 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 and examinations.

For an overview survey of separation logic (in postscript), click here.

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.

An Overview, January 19

Hoare Logic, revised February 1

Basic Separation Logic revised February 9

Lists and List Segments, February 11

Iterated Separating Conjunction, February 18

Trees and Dags, February 18

Special Classes of Assertions, Revised May 10

Homework Assignments (in Postscript)

Assigned February 9, due February 18

Assigned February 16, due February 25

Assigned February 25, due March 3

Last updated: June 5, 2005