Starling is an automated verification tool for concurrent programs. It accepts programs written in a C-like language and annotated with Concurrent Views Framework-style assertions, as well as a series of constraints binding those assertions to concrete facts about the program's shared state, and tries to prove soundness.
For a quick example of the flavour of Starling scripts, see
Starling is a work in progress, but currently it can check correctness of fully-specified programs written in a limited command language (integer and Boolean variables; arrays; basic statements; atomic assignment and compare-and-swap; parameter-less methods with no calling).
Starling can be used on its own to check complete proofs of programs
Z3 SMT solver, or combined with other tools:
- With the
HSFHorn clause solver, Starling can perform limited definition inference for proofs, helping to complete partial proofs;
- (Experimental.) With the
GRASShopperseparation logic solver, Starling can prove properties of programs using linked heap-based data structures.
- Methods with call/return syntax;
- Proof of soundness of the tool itself;
- Clean-up and general user interface polish.
A F# 4.0 development environment (tested with mono on Linux), NuGet, and the native Z3 library for your platform.
NuGet should be able to restore the rest of the prerequisites.
The helper scripts mentioned below require a POSIX environment: cygwin or MSYS should work on Windows.
To use HSF, you will need a copy of
qarmc. An outdated but
useable version of
is available. Install it in your
PATH to be able to use
To use GRASShopper, you will need a copy of
This can be compiled from source available at
this GitHub repository. Install it
PATH to be able to use
- To check a Starling file using Z3, use
./starling.sh -ssmt-failures /path/to/file. Examples using Z3 can be found in
- To check a Starling file using HSF/qarmc, use
./starling-hsf.sh /path/to/file. Examples using HSF can be found in
- To check a Starling file using
./starling-gh.sh /path/to/file. Examples using GRASShopper can be found in
- To run the regression tests, use
A very basic major mode (highlighting only) for GNU Emacs, based on
is available in
syntax/starling-mode.el. This is fairly outdated.