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

Download the source code (latest release: 1.01)

Note: SmallfootRG is now obsolete and is no longer maintained; please consider using CAVE instead.


Related publications

  1. 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.
  2. 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.

Related tools

Imprint | Data protection