2 \page other-tools Other Tools
4 \author Martin Brain, Peter Schrammel
8 FIXME: The text in this section is a bit outdated.
10 The CPROVER subversion archive contains a number of separate programs.
11 Others are developed separately as patches or separate
12 branches.Interfaces are have been and are continuing to stablise but
13 older code may require work to compile and function correctly.
17 * `CBMC`: A bounded model checking tool for C and C++. See
20 * `goto-cc`: A drop-in, flag compatible replacement for GCC and other
21 compilers that produces goto-programs rather than executable binaries.
24 * `goto-instrument`: A collection of functions for instrumenting and
25 modifying goto-programs. See \ref goto-instrument.
27 Model checkers and similar tools:
29 * `SatABS`: A CEGAR model checker using predicate abstraction. Is
30 roughly 10,000 lines of code (on top of the CPROVER code base) and is
31 developed in its own subversion archive. It uses an external model
32 checker to find potentially feasible paths. Key limitations are
33 related to code with pointers and there is scope for significant
36 * `Scratch`: Alistair Donaldson’s k-induction based tool. The
37 front-end is in the old project CVS and some of the functionality is
40 * `Wolverine`: An implementation of Ken McMillan’s IMPACT algorithm
41 for sequential programs. In the old project CVS.
43 * `C-Impact`: An implementation of Ken McMillan’s IMPACT algorithm for
44 parallel programs. In the old project CVS.
46 * `LoopFrog`: A loop summarisation tool.
48 * `TAN`: Christoph’s termination analyser.
52 * `cover`: A basic test-input generation tool. In the old
55 * `FShell`: A test-input generation tool that allows the user to
56 specify the desired coverage using a custom language (which includes
57 regular expressions over paths). It uses incremental SAT and is thus
58 faster than the naïve “add assertions one at a time and use the
59 counter-examples” approach. Is developed in its own subversion.
61 Alternative front-ends and input translators:
63 * `Scoot`: A System-C to C translator. Probably in the old
66 * `???`: A Simulink to C translator. In the old project CVS.
68 * `???`: A Verilog front-end. In the old project CVS.
70 * `???`: A converter from Codewarrior project files to Makefiles. In
75 * `ai`: Leo’s hybrid abstract interpretation / CEGAR tool.
77 * `DeltaCheck?`: Ajitha’s slicing tool, aimed at locating changes and
78 differential verification. In the old project CVS.
80 There are tools based on the CPROVER framework from other research
81 groups which are not listed here.