Book details
Software Foundations Vol 6: Separation Logic Foundations
Categories Software engineering
A mechanized introduction to separation logic, developed through formal definitions, proofs, and Coq exercises. It treats reasoning about mutable state and heap-manipulating programs, including the logic’s assertion language and proof principles.