Foundations of Separation Logic
Introduction to using separation logic to reason about sequential imperative programs in Coq.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Volume 6: Separation Logic Foundations softwarefoundations.cis.upenn.edu
An introduction to separation logic and how to build program verification tools on top of it.
-
Program Logics for Certified Compilers cs.princeton.edu
Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples.
-
-
CertiGraph github.com
Library for reasoning about directed graphs and their embedding in separation logic.
-
Program Logics github.com
Companion Coq sources for a course on program logics at Collège de France.
-
Hoare Type Theory github.com
A shallow embedding of sequential separation logic formulated as a type theory.
Coq › Resources > Course Material: “Introduction to using separation logic to reason about sequential imperative programs in Coq.”