15-818A4 Current Research on Separation Logic

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