Tools

On this page we make available binaries for the tools QPROVER and PROBITY, developed for the thesis. For a more elaborate description of the tools we refer to the thesis itself.

Binaries

Usage

For each tool, we use a variant of goto-cc, namely goto-cc-qprover and goto-cc-probity to compile ANSI-C source code. Generally, we can use these compilers instead of gcc, with the same command-line options, etc. Instead of an executable binary, these compilers generate a goto-cc binary.

QPROVER Then, for QPROVER, the binary qprover is the main model checker. This model checker takes a goto-cc binary and model checks it. We describe some command-line parameters of this model checker.

• --cost: compute a cost property (probabilistic reachability properties are checked without this switch)
• -b min: compute a minimum bound (maximum bounds are computed without this switch)
• -C nearest: use the nearest refinable state selection heuristic
• -C coarsest: use the coarest refinable state selection heuristic
• -P predecessors: use the PrecAdd predicate propagation heuristic
• -P trace: use the TraceAdd predicate propagation heuristic
• --satabs: perform predicate initialisation by running SATABS first
• --no-opt4: disable the reachable state restriction optimisation

PROBITY For PROBITY, the binary probity is the main model checker. This binary depends on the (adapted) safety checker binary wolver. We describe various command-line arguments to this tool:

• --path-length-threshold: the number of conditional statements we expand before checking feasibility (in experiments we used a seting of 1)
• --path-length-threshold: the maximum number of times we call ForceCover every time we consider an unwinding node (in experiments we used a setting of 20)
• --no-heuristics: disables the greedy exploration heuristic
• --templates: enables the template extension