Scratch is a model checker for detecting DMA races in software for the Cell BE processor. The tool uses bounded model checking to detect DMA races, and bounded model checking with k-induction to prove absence of races.

For questions about Scratch contact

You should also read the license.


We currently distribute binaries for 64-bit Linux only.

Date x86 Windows Linux
on request

For instructions on how to use Scratch, run the tool as follows:

scratch --help

Alternatively, have a look at the scripts supplied with each of the benchmark examples, available below.

Benchmarks for TACAS submission

You can either navigate the benchmarks online, or download an archive of benchmarks to try out with the tool.

Each benchmark is in its own folder, with common files located in the root folder.

To run a particular benchmark, navigate to its folder and type:




This research is supported by a grant from EPSRC.