A generalization of the notion of fractional permissions for tracking the ownership of shared resources and, in particular, to track when a resource goes back to having a single owner.
Includes fractional permissions and permission counting.
Adapted for separation logic by bornat:popl:2005. Later, heule:ftfjp:2011 developed a variation that avoids the sometimes ad hoc choice of what fractions to use.
Notes related to Permission accounting
Papers related to Permission accounting
- Leveraging Rust types for modular specification and verification [astrauskas:oopsla:2019]
- Permission accounting in separation logic [bornat:popl:2005]
- Fractional permissions without the fractions [heule:ftfjp:2011]
- VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
- VeriFast: Imperative programs as proofs [jacobs:vstte:2010]
- Verification of concurrent programs with Chalice [leino:fosad:2007]