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
- defining predicates. Instead predicates for lists, trees and xor-lists were hardwired in the tool.
- permission accounting
And there seems to be no arithmetic in the examples so I suspect that it was not using an SMT solver in the background.
Papers related to Smallfoot: Modular automatic assertion checking with separation logic
- Symbolic execution with separation logic [berdine:aplas:2005]
- Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]