Scratch

Scratch

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 alastair.donaldson@comlab.ox.ac.uk.

You should also read the license.

Download

We currently distribute binaries for 64-bit Linux only.

Date x86 Windows Linux
8-Oct-2009
on request
scratch-0.1-linux-x86-64.tar.gz

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:

./run_scratch_on_buggy_version

or

./run_scratch_on_correct_version

This research is supported by a grant from EPSRC.