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.

  • Dowload the summary paper entitled Separation Logic for Sequential Programs. This paper, presented at ICFP'20, covers most of the material with the notable exception of the weakest precondition generator.
  • Browse the course files, in HTML format.
  • Download the course material, which includes Coq and HTML files.
  • The files should work with all versions from Coq v8.8 to coq v8.12. Please contact me in case of issues.
  • Compilation issues warnings with versions 8.10 or above; these warnings may be safely ignored.
  • See the README file for instructions.
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.