Foundations of Separation Logic

The Foundations of Separation Logic course presents the foundations of Separation Logic for sequential programs and the construction of a practical program verification tool based on Separation Logic.

The course material is entirely developed in the Coq proof assistant, following the style of the Software Foundations volumes.

Solutions are available on demand. Contributions to the material are welcome.

Older material: Master course on Separation Logic

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.