K-Inductor

K-Inductor is a software model checker C programs that uses k-induction. Induction is applied to loops in an input program, and loop-free base and step cases are passed to the CBMC tool for bit-blasting.

For questions about K-Inductor contact alastair.donaldson@comlab.ox.ac.uk.

You should also read the license.

Download

We currently distribute binaries for 64-bit Linux only; other binary formats are available on request.

Date

x86 Windows

Linux

8-Oct-2010

on request

k-inductor-1.0-linux-x86-64.tar.gz

For instructions on how to use K-Inductor, run the tool as follows:

kinductor --help

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

Benchmarks for ESOP submission

The ESOP benchmarks use the SCRATCH tool, which incorporates K-Inductor, for DMA race analysis.

To try the benchmarks, download SCRATCH and add it to your path. Then download and unpack the 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, go to the spu directory for the given benchmark in the archive. To run the benchmark in serial, type:

./runtest --[strategy]

where strategy is one of: monolithic, inward-1, inward-all, outward-1 or outward-all, as described in the ESOP submission.

To run the benchmark in parllel, add --parallel --nthreads N, where N is the number of threads you wish to use.

This research is supported by a grant from EPSRC.