Separation logic is an extension of Hoare logic that adds the ability to reason about heap-based data structures and, in particular, about aliasing. It does this using ideas from linear logic to model resources that cannot be duplicated.
Variations on the theme of separation logic have been developed and are collectively referred to as permission logic.
Many tools that use separation logic only use a subset because some parts of separation logic like “magic wands” (linear implication) have poor complexity/decidability properties. In particular, tools often keep the linear and the classical parts of a term separate.
Automatic tools that use separation logic (e.g., calcagno:sas:2006 and related papers) often use abstract interpretation and use an even smaller subset of separation logic as their abstract domains together with more conventional widening operators, fixpoints, etc. This lets them construct a shape analysis where separation logic terms are used to capture what is known about the shape of a data structure. And it lets them move back and forth between precise reasoning using symbolic execution outside of loops and deliberately dropping information using abstract interpretation when generalizing loop bodies into loops / loop invariants.
Auto-active tools like the VeriFast verifier typically use more of the logic (but still not all of it) and require the user to provide loop invariants.
Notes related to Separation logic
Bi-abduction, Concurrent separation logic, Fractional permissions, Frame rule, Implicit dynamic frames, Magic wand, Permission accounting, Permission logic, Smallfoot verifier, Symbolic execution, VeriFast verifier
Papers related to Separation logic
- The meaning of memory safety [azevedo:post:2018]
- Symbolic execution with separation logic [berdine:aplas:2005]
- Shape analysis for composite data structures [berdine:cav:2007]
- Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
- Permission accounting in separation logic [bornat:popl:2005]
- Beyond reachability: Shape abstraction in the presence of pointer arithmetic [calcagno:sas:2006]
- A local shape analysis based on separation logic [distefano:tacas:2006]
- Behavioral interface specification languages [hatcliff:compsurv:2012]
- 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]
- High-level separation logic for low-level code [jensen:popl:2013]
- Software model checking [jhala:compsurv:2009]
- Coq: The world's best macro assembler? [kennedy:ppdp:2013]
- Generalized symbolic execution for model checking and testing [khurshid:tacas:2003]
- Verifying event-driven programs using ramified frame properties [krishnaswami:tldi:2010]
- 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]
- RefinedC: Automating the foundational verification of C code with refined ownership types [sammler:pldi:2021]
- Lightweight support for magic wands in an automatic verifier [schwerhoff:ecoop:2015]
- Implicit dynamic frames: Combining dynamic frames and separation logic [smans:ecoop:2009]
- Local reasoning about while-loops [tuerk:vstte:2010]
- Annotation inference for separation logic based verifiers [vogels:fmoods:2011]