Separation Logic Course
I teach at the MPRI
(Parisian Master of Research in Computer Sciences), the program verification course, together with Claude Marché.
I cover 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.
Slides from Febuary 2017: