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.
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.
MIT; see LICENSE.md.