Separation Logic

Separation Logic

Separation logic, first developed by O'Hearn and Reynolds,
is an extension of Hoare's logic which addresses
reasoning about programs that access and mutate data structures.
It includes a "frame rule" which
enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.
Local reasoning helps with the scalability of proofs done in automatic and semi-automatic verification and program analysis tools.
Separation logic has also been applied to concurrent systems, using the separating conjunction to
divide reasoning amongst processes or threads in order to make reasoning more efficient.

The purpose of these pages is to give some context for people wanting to learn about the work. There is no attempt to be comprehensive or uptodate, but you can find lots of information to get started on the pages linked at the top.

Quick Start: A good way to get started is to read the CSL'01 paper which introduced the principle of local reasoning, and Reynolds's invited survey paper from LICS'02, together or in quick succession. When understanding a subject it is also helpful (and not emphasized enough in CS) to have a picture of the development of ideas. If you are interested in this sort of thing, go here for the early days.

Surveys, Courses, etc

- A Primer on Separation Logic (and Automatic Program Verification and Analysis). Peter O'Hearn. Paper accompanying Marktoberdorf 2011 PhD school course on Separation Logic and Automatic Program Verification
- John Reynolds's 2011 graduate course on SL at CMU
- ENS 2011 Winter School on Separation Logics and Applications. (includes lots on concurrency) Alexey Gotsman, Matthew Parkinson, Hongseok Yang
- Separation Logic and Modalities: A survey. S Demri and M Deters