Separation Logic Foundations

The Separation Logic Foundations course presents the foundations of Separation Logic and the construction of a practical program verification tool based on Separation Logic, in the spirit of CFML.
The course material is entirely developed in the Coq proof assistant, following the style of the Software Foundations volumes.
  • Download the course material (includes Coq and HTML files).
  • The files compile with Coq v8.8 and v8.9. They also compile with Coq v8.10 and v8.11, with warnings that can be ignored.
  • See the README file for instructions.
Solutions are available on demand. Contributions to the material are welcome.

Separation Logic Course at MPRI

I taught from 2013 until 2017 at the MPRI (Parisian Master of Research in Computer Sciences), the program verification course, together with Claude Marché. The course covered the following chapters:
  • Heap predicates, heap entailment, interpretation triples, derivation rules.
  • Representation predicates for list and trees, nested mutable data structures, ownership transfer.
  • Reasoning about loops, frame during loops, higher-order functions, iterators.
  • Arrays, records and objects, frame over individual cells, data structures with sharing.
  • Extensions of Separation Logic for read-only permissions, parallelism, concurrency, and amortized analysis.
  • Characteristic formulae for integrating Separation Logic in Coq.

Here are the slides from Febuary 2017:

A similar course is now taught by Jean-Marie Madiot.