Permission accounting in separation logic

By Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson. ACM-SIGACT Symposium on Principles of Programming Languages, 2005

454 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.

VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java (2011, background): “For this scenario, another permission accounting scheme known as counting permissions [3] is appropriate.”
Smallfoot: Modular Automatic Assertion Checking with Separation Logic (2005, background): “It is useful to use the intuition of “permission to access” to describe this [9, 8]: the permission to access the pointer moves from the first to the second process along with the pointer value.”
Local Action and Abstract Separation Logic (2007, background): “In contrast , the algebra (0, 1] does allow such conversion using identities such as 1/2 + 1/2 = 1; see [8].”
VCC: A Practical System for Verifying Concurrent C (2009, background): “Later, Bornat proposed a fractional ownership scheme to allow for shared readonly state also [22].”
Iris from the ground up: A modular foundation for higher-order concurrent separation logic (2018, unknown): “For example, considering the points-to connective ` q7−→ v with a fractional permission q (Boyland, 2003; Bornat et al., 2005), the proposition ∃q. ` q7−→ v is duplicable (which follows from halving the fractional permission q), but it is not persistent.”
Resources, Concurrency and Local Reasoning (2004, background): “[Aside: There is a possibility of terminological inconsistency in the use of “resource”, summed up as follows by Richard Bornat, writing in [ 5 ].”