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], prepared with Isabelle version 2009-2, or browse the pretty-printed sources online:

Coq proofs

Click here for the online documentation with the proofs hidden, or here for the version with the proofs visible.

Valid XHTML 1.0 Strict