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.

Related Papers


Josh Berdine
Cristiano Calcagno
Peter W. O'Hearn