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]