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.
|linux binaries (x86_64)||linux binaries (x86_64)|
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.
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: