Foundations of Separation Logic
The Foundations of Separation Logic 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.
SF: Volume 6 of the Software Foundations series — Reference book, all in Coq, May 2021
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
Habilitation manuscript, March 2023