Smallfoot is an automatic verification tool that checks separation logic specifications of sequential and concurrent programs that manipulate recursive dynamically-allocated (linked) data structures.
Smallfoot 0.1 is distributed as a source tarball (MD5 checksum) under the QPL. Objective Caml (version 3.07 or later) is needed to compile it. There are no additional source dependencies. Additionally, the distribution includes precompiled MacOS X PPC and Linux x86 executables.
Here is a precompiled Win32 executable.
For further information, and a description of the input language, see the README.
See also SmallfootRG, which extends Smallfoot with Vafeiadis and Parkinson's combination of rely/guarantee and separation logic.
Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. A Decidable Fragment of Separation Logic. (with proofs)
In K. Lodaya and M. Mahajan (Eds.): FSTTCS 2004, LNCS 3328, pp. 97-109, 2004.
