This paper describes the proof-theoretic basis for the Smallfoot verification tool described in a companion paper. See the other paper for a description.
Papers related to Symbolic execution with separation logic
- Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
- A local shape analysis based on separation logic [distefano:tacas:2006]