A Semantics for Concurrent Separation Logic

By S. Brookes. International Conference on Concurrency Theory, 2004

357 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Local Action and Abstract Separation Logic (2007, background): “Soundness of the concurrent logic was very difficult to come by, originally, even for a particular separation algebra (the RAM model); it was proven in a remarkable work of Brookes [12].”
Permission accounting in separation logic (2005, methodology): “This approach has been proved sound by Brookes in [6]: the result is that given invariant formulae for each bundle and (?)-separation of bundle resources from each other and from thread resources, we can reason sequentially about each thread and the CCRs it employs.”
Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, background): “It also supports annotations for concurrency, following a concurrent extension of separation logic [31, 11].”
A Marriage of Rely/Guarantee and Separation Logic (2007, background): “Brookes has shown concurrent separation logic to be sound [3].”