This page is about a new soundness proof for concurrent separation logic (CSL)
in terms of the standard operational semantics. The new proof gives a direct
meaning to CSL judgments, explains clearly the problem with the conjunction
rule and "precise" resource invariants, and can easily be adapted to handle
extensions of CSL, such as permissions and storable locks, as well as more
advanced program logics, such as RGSep.
Concurrent separation logic and operational semantics.
In MFPS 2011. ENTCS 276, pp. 335-351. Elsevier (September 2011)
[Paper]
[@Elsevier]
[Slides]
Isabelle proofs
Click here for the tarball [.zip], ported to Isabelle version 2016-1 by Qin Yu and James Brotherston, or browse the pretty-printed sources online:
- Lang: The programming language and its semantics
- CSLsound: Soundness proof of concurrent separation logic
- Perm: Soundness proof of CSL + permissions
Rocq proofs
The soundness proofs of CSL and RGSep have also been carried out using the Rocq Prover. They are available in this Github repository.