Separation Logic Foundations
The Separation Logic Foundations course presents the foundations of Separation Logic and the construction of a practical program verification tool based on Separation Logic, in the spirit of CFML.
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.
Separation Logic Course at MPRI
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:
Here are the slides from Febuary 2017:
A similar course is now taught by Jean-Marie Madiot.