Smallfoot: Modular automatic assertion checking with separation logic

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

Formal Methods for Components and Objects
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 115-137
Topic(s): tools verification
Note(s): separation logic, permission logic, smallfoot verifier, symbolic execution, VeriFast verifier
Papers: berdine:aplas:2005, jacobs:nfm:2011, parkinson:popl:2005, bornat:popl:2005

Smallfoot is a tool for automatically verifying both sequential and concurrent heap-manipulating programs that is based on (concurrent) separation logic and symbolic execution. The proof theoretic foundations of the tool are described in a companion paper.

One of the key tricks in enabling automation is to greatly simplify the expressive power of the logic so that the symbolic state consists of a set of pure formulae about non-heap values plus a list of spatial formulae that describe the heap.

The paper explicitly avoids describing how conditionals are handled but, I believe that it works like the later VeriFast by path splitting: separately exploring the path that starts with the “then” branch and the path that starts with the “else” branch. This seems to be necessary because there is no mention of what to do at join points and because there seems to be no way to represent disjunctions of spatial formulae.

The version of Smallfoot described here did not have support for

And there seems to be no arithmetic in the examples so I suspect that it was not using an SMT solver in the background.