## Foundations of Separation LogicThe 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 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 compile with all versions from Coq v8.8 to coq v8.11,
and even Coq's master branch (though possibly with a few warnings). - See the README file for instructions.
Solutions are available on demand. Contributions to the material are welcome.
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. |