SmallfootRG

SmallfootRG is memory safety checker for concurrent singly linked list programs that is based on RGSep and Smallfoot.

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.