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.

Viktor Vafeiadis: Concurrent separation logic and operational semantics. In MFPS 2011.

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:

Coq proofs

The soundness proofs of CSL and RGSep have also been carried out using the Coq proof assistant. They are available in this Github repository.

Valid XHTML 1.0 Strict