Symbolic execution with separation logic

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 15 February 2020

Programming Languages and Systems
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 52-68
2005
Topic(s): verification
Note(s): permission logic, separation logic, smallfoot verifier, symbolic execution
Papers: berdine:fmco:2005

This paper describes the proof-theoretic basis for the Smallfoot verification tool described in a companion paper. See the other paper for a description.