A tool for verifying C/C++ program transformations. Based on Alloy.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
alloy
examples
.gitignore
INSTALL.md
LICENSE.md
README.md
alloy-mod.jar
alloy.sh
genall.sh
gentest.sh
main.fs
packages.config
parser.fs
runtest.sh
stellite-tool.fsproj
stellite-tool.sln
stellite.sh
test.sh
translator.fs

README.md

Stellite

A tool for converting C11-style program transformations into an Alloy model, and then checking the transformation's validity. Built using F# and FParsec.

Portions of Stellite's code were adapted with permission from Starling.

A draft paper on the theory underlying Stellite is available here.

Usage

Stellite takes optimisations written in a simple C-like language: see examples/pass/RxlRxl-Rxl.stl for an instance.

To check a single example, call

$ ./runtest.sh <size> examples/pass/RxlRxl-Rxl.stl

To check all the examples in examples/pass and examples/fail, call

$ ./test.sh <size>

The parameter <size> is the maximum number of memory actions in the checked histories. Size 8 is sufficient for most of our examples.

People

License

MIT; see LICENSE.md.