cprover
/builddir/build/BUILD/cbmc-cbmc-5.11/doc/architectural/other-tools.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page other-tools Other Tools
3 
4 \author Martin Brain, Peter Schrammel
5 
6 # Other Tools
7 
8 FIXME: The text in this section is a bit outdated.
9 
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.
14 
15 In the main archive:
16 
17 * `CBMC`: A bounded model checking tool for C and C++. See
18  \ref cbmc.
19 
20 * `goto-cc`: A drop-in, flag compatible replacement for GCC and other
21  compilers that produces goto-programs rather than executable binaries.
22  See \ref goto-cc.
23 
24 * `goto-instrument`: A collection of functions for instrumenting and
25  modifying goto-programs. See \ref goto-instrument.
26 
27 Model checkers and similar tools:
28 
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
34  improvement.
35 
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
38  in `goto-instrument`.
39 
40 * `Wolverine`: An implementation of Ken McMillan’s IMPACT algorithm
41  for sequential programs. In the old project CVS.
42 
43 * `C-Impact`: An implementation of Ken McMillan’s IMPACT algorithm for
44  parallel programs. In the old project CVS.
45 
46 * `LoopFrog`: A loop summarisation tool.
47 
48 * `TAN`: Christoph’s termination analyser.
49 
50 Test case generation:
51 
52 * `cover`: A basic test-input generation tool. In the old
53  project CVS.
54 
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.
60 
61 Alternative front-ends and input translators:
62 
63 * `Scoot`: A System-C to C translator. Probably in the old
64  project CVS.
65 
66 * `???`: A Simulink to C translator. In the old project CVS.
67 
68 * `???`: A Verilog front-end. In the old project CVS.
69 
70 * `???`: A converter from Codewarrior project files to Makefiles. In
71  the old project CVS.
72 
73 Other tools:
74 
75 * `ai`: Leo’s hybrid abstract interpretation / CEGAR tool.
76 
77 * `DeltaCheck?`: Ajitha’s slicing tool, aimed at locating changes and
78  differential verification. In the old project CVS.
79 
80 There are tools based on the CPROVER framework from other research
81 groups which are not listed here.