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

### John C. Reynolds

First Half of Spring Semester 2009
University Units: 6 (minicourse)

Mondays and Wednesdays noon-1:20 pm Wean Hall 4623

### Course Description

Separation logic, first developed by O'Hearn and Reynolds,
is an extension of Hoare logic originally intended for reasoning about
programs that use shared mutable data structures. It is based on the
concept of separating conjunction, which permits the concise expression
of aliasing constraints.
More generally, the logic provides a "frame rule", which enables local
reasoning that is the key to the scalability of proofs. Examples of
nontrivial proofs include the Schorr-Waite marking algorithm and the
Cheney relocating garbage collector.

Recently, by generalizing the concept of storage access to ownership and
permissions, the logic has been extended to encompass information hiding,
shared-variable concurrency, and numerical permissions.

We will survey the current development of separation logic, including,
as time permits, extensions to unrestricted address arithmetic, dynamically
allocated arrays, recursive procedures, shared-variable concurrency, and
read-only sharing.

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 of separation logic, see the first chapter and bibliography
of the course notes below.

### NOTICES

Late homework will not be accepted. However, the lowest homework grade for
each student will be disregarded in computing their average.
Exercises 3, 4, and 5 in Chapter 4 of the notes will be due
Monday, February 23.

### Course Notes (in PDF)

LINK TO FOLLOWING MINICOURSE (15-818A4)
Last updated: February 17, 2009