## 15-818A4 Current Research on Separation Logic
(6 units)
Spring 2011

### John C. Reynolds

Second Half of Spring Semester 2011 (starting March 14)
University Units: 6 (research minicourse)

Gates-Hillman Center 4211

Mondays, Wednesdays, and Fridays 12:30 pm-1:20 pm

### Course Description

We will study and discuss recent papers on separation logic
and related topics.
Anyone who is interested can attend, and you are welcome to come just for
papers you are particularly interested in. I'll post the progress of the
course on the class webpage, which is linked from my home page at
http://cs.cmu.edu/~jcr. Some familiarity with separation logic and Hoare
logic will be needed (such as provided in 15-818A3 - Introduction to Separation
Logic).

TEXTS: Papers and notes to be distributed in class.

METHOD OF EVALUATION: Each creditor will be required to lecture on a paper
chosen by them and the instructor.

### Papers and Videos of Lectures

(1) Peter W. O'Hearn. Resources, Concurrency, and Local Reasoning. TCS
375(1-3):271-307, May 2007.
Lecture 22,
Lecture 23,
Lecture 24,
Lecture 25

(2) Stephen D. Brookes. A Semantics for Concurrent Separation Logic.
TCS 375(1-3):227-270, May 2007. (Lectures by Stephen Brookes)

Lecture 26,
Lecture 27

(3) Richard Bornat, Cristiano Calcagno, O'Hearn, and Matthew Parkinson.
Permission Accounting in Separation Logic. POPL 2005, 259-270.

Lecture 28,
Lecture 29,
Lecture 30 (first part)

(4) Parkinson, Bornat, Calcagno. Variables as Resource in Hoare Logic.
LICS 21 2006.

Lecture 30 (second part),
Lecture 31,
Lecture 32,
Lecture 33

(5) Calcagno, O'Hearn, and Hongseok Yang. Local Action and Abstract Separation Logic. LICS 22 366-378, July 2007.

Lecture 34,
Lecture 35,
Lecture 36

(6) Yang. Relational Separation Logic. TCS 375(1-3):308-334, May 2007. (Lectures by Bernardo Toninho)

Lecture 37,
Lecture 38

(7) Uday S. Reddy. Syntactic Control of Interference for Separation Logic (Preliminary Report) April 12, 2011.

Lecture 39

(8) Parkinson, Bornat, and O'Hearn. Modular Verification of a Non-Blocking Stack. POPL 2007.
(Lectures by Henry DeYoung)

Lecture 40,
Lecture 41

(9) John C. Reynolds. Automatic Computation of Static Variable Permissions. MFPS 2011. (The class lecture was a
preliminary version of the talk at MFPS.)

Lecture 42

### Handouts

An Application of Auxiliary Variables,
March 17

A Concurrent Cyclic Buffer,
revised March 22

Permission Accounting in Separation Logic,
March 28

Oddities of Inductive Definitions,
revised April 1

Variables as Resources - An Example,
April 1

Comments on Rules for Variables as Resources,
revised April 4

Variables as Resources in Hoare Logics (slides),
revised April 11

Modular Verification of a Non-Blocking Stack (slides),
April 25

An Inference Procedure for Static Variable Permissions (slides),
These slides have been obsoleted by
Automatic Computation of Static Variable Permissions,
MFPS, May 28

LINK TO PREVIOUS MINICOURSE (15-818A3)
Last updated: August 7, 2011