cprover
cbmc/README.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \defgroup cbmc cbmc
3 
4 # Folder CBMC
5 
6 \author Martin Brain
7 
8 This contains the first full application. CBMC is a bounded model
9 checker that uses the front ends (`ansi-c`, `cpp`, goto-program or
10 others) to create a goto-program, `goto-symex` to unwind the loops the
11 given number of times and to produce and equation system and finally
12 `solvers` to find a counter-example (technically, `goto-symex` is then
13 used to construct the counter-example trace).