SmallfootRG
SmallfootRG is an automatic verification tool that takes a lightly annotated
program and attempts to prove that the input program is memory safe and
has no memory leaks. The user is expected to annotate the program with
preconditions, postconditions, and a description of the inteference due to
concurrency. Interference is described using sets of actions.
Loop invariants may be provided, but are otherwise inferred.
SmallfootRG 1.0 is distributed as a source
tarball
under the
QPL.
Objective Caml (version
3.07 or later) is needed to compile it. There are no additional source
dependencies.
This is a development release, intended only for experimentation.
The distribution contains contains a README file that describes the input
language and a collection of sample programs to try.
For further information please contact
Viktor Vafeiadis or
Matthew Parkinson.
See also the original release of
Smallfoot,
upon which SmallfootRG is based.
Related Papers