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.
Peter W. O'Hearn