Permission logic is a generalization of separation logic. All permission logics have
- a notion of resource
- resources follow rules of linear logic wrt replication / consumption
Permission logics include
- many variants of separation logic
- implicit dynamic frames
Systems based on permission logic:
Notes related to Permission logic
Boogie verifier, Chalice verifier, Fractional permissions, Implicit dynamic frames, Magic wand, Permission accounting, Prusti verifier, RustBelt verifier, Separation logic, Viper verifier
Papers related to Permission logic
- Leveraging Rust types for modular specification and verification [astrauskas:oopsla:2019]
- Symbolic execution with separation logic [berdine:aplas:2005]
- Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
- Witnessing the elimination of magic wands [blom:ijsttt:2015]
- Permission accounting in separation logic [bornat:popl:2005]
- A semantics for concurrent separation logic [brookes:tcs:2006]
- Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]
- Enforcing high-level protocols in low-level software [deline:pldi:2001]
- Views: Compositional reasoning for concurrent programs [dinsdale-young:popl:2013]
- A local shape analysis based on separation logic [distefano:tacas:2006]
- Fractional permissions without the fractions [heule:ftfjp:2011]
- Abstract read permissions: Fractional permissions without the fractions [heule:vmcai:2013]
- The ramifications of sharing in data structures [hobor:popl:2013]
- VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
- VeriFast: Imperative programs as proofs [jacobs:vstte:2010]
- RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
- Dynamic frames: Support for framing, dependencies and sharing without restrictions [kassios:fm:2006]
- Verifying event-driven programs using ramified frame properties [krishnaswami:tldi:2010]
- Verification of concurrent programs with Chalice [leino:fosad:2007]
- Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]
- Ynot: Dependent types for imperative programs [nanevski:icfp:2008]
- Specifying concurrent programs in separation logic: Morphisms and simulations [nanevski:oopsla:2019]
- Separation logic [ohearn:cacm:2019]
- Resources, concurrency, and local reasoning [ohearn:tcs:2007]
- Separation logic and abstraction [parkinson:popl:2005]
- Sound formal verification of Linux's USB BP keyboard driver [penninckx:nfm:2012]
- Software verification with VeriFast: Industrial case studies [philippaerts:scp:2014]
- Separation logic: a logic for shared mutable data structures [reynolds:lics:2002]
- Lightweight support for magic wands in an automatic verifier [schwerhoff:ecoop:2015]
- Implicit dynamic frames: Combining dynamic frames and separation logic [smans:ecoop:2009]
- Heap-dependent expressions in separation logic [smans:fmood:2010]
- Alias types [smith:esop:2000]
- Annotation inference for separation logic based verifiers [vogels:fmoods:2011]
- Alias types for recursive data structures [walker:tic:2001]