Separation Logic Foundations

The Separation Logic Foundations 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.

Related publications

Arthur Charguéraud
SF: Volume 6 of the Software Foundations series — Reference book, all in Coq, May 2021
Arthur Charguéraud
ICFP: International Conference on Functional Programming, August 2020
Published in the journal Proceedings of the ACM on Programming Languages (PACMPL)
Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter
TOPLAS: ACM Transactions on Programming Languages and Systems, March 2023
Arthur Charguéraud
Habilitation manuscript, March 2023

Older teacher 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.