Program Verification

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.

Contents of the course available from the Software Foundations website.
Companion course notes formatted using LaTeX.
More advanced material is covered in my habilitation manuscript.

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

Related publications

Separation Logic Foundations

Arthur Charguéraud

SF: Volume 6 of the Software Foundations series — Reference book, all in Coq, May 2021

website

Separation Logic for Sequential Programs

Arthur Charguéraud

ICFP: International Conference on Functional Programming, August 2020

Published in the journal Proceedings of the ACM on Programming Languages (PACMPL)

paper - abstract - course material - talk video

Omnisemantics: Smooth Handling of Nondeterminism

Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter

TOPLAS: ACM Transactions on Programming Languages and Systems, March 2023

paper - artifact

A Modern Eye on Separation Logic for Sequential Programs

Arthur Charguéraud

Habilitation manuscript, March 2023

paper - abstract

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.