SmallfootRG is memory safety checker for concurrent singly linked list programs
that is based on RGSep and
Download the source code (latest release: 1.01)
Note: SmallfootRG is now obsolete and is no longer maintained;
please consider using CAVE instead.
Viktor Vafeiadis, Matthew Parkinson.
A marriage of rely/guarantee and separation logic.
In CONCUR 2007. LNCS, vol. 4703, pp. 256-271. Springer (Sep. 2007)
This paper describes RGSep, the underlying logic used by SmallfootRG.
Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis.
Modular safety checking for fine-grained concurrency.
In SAS 2007. LNCS, vol. 4634, pp. 233-238. Springer (Aug. 2007)
This paper describes the core symbolic execution and stabilization procedures used by SmallfootRG.
- CAVE: a linearisability prover for concurrent singly
linked list programs.
- TVLA is a generic static
analyser for 3-valued logic domains and has been used to prove properties of
concurrent algorithms, including linearizability if the linearization points are
specified by the used.