diff options
Diffstat (limited to 'development/cbmc/README')
| -rw-r--r-- | development/cbmc/README | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/development/cbmc/README b/development/cbmc/README new file mode 100644 index 0000000000..07735ff04f --- /dev/null +++ b/development/cbmc/README @@ -0,0 +1,37 @@ +CBMC is a Bounded Model Checker for C and C++ programs. +It supports C89, C99, most of C11/C17 and most compiler extensions +provided by gcc, clang, and Visual Studio. A variant of CBMC that +analyses Java bytecode is available as JBMC. +[Set JBMC=ON to enable JBMC.] + +CBMC verifies memory safety (which includes array bounds checks +and checks for the safe use of pointers), checks for exceptions, +checks for various variants of undefined behavior, and +user-specified assertions. Furthermore, it can check C and C++ for +I/O equivalence with other languages, such as Verilog. The +verification is performed by unwinding the loops in the program +and passing the resulting equation to a decision procedure. + +CBMC comes with a built-in solver for bit-vector formulas that is +based on MiniSat. As an alternative, CBMC has featured support for +external SMT solvers since version 3.3. The solvers we recommend +are (in no particular order) Boolector, CVC5 and Z3. Note that +these solvers need to be installed separately and have different +licensing conditions. +[This SlackBuild builds Cadical as the internal solver.] + +If you need a Model Checker for Verilog or SMV files, consider +EBMC. For Java, use JBMC. + +This research was sponsored by the Semiconductor Research +Corporation (SRC) under contract no. 99-TJ-684, the National +Science Foundation (NSF) under grant no. CCR-9803774, the Office +of Naval Research (ONR), the Naval Research Laboratory (NRL) under +contract no. N00014-01-1-0796, and by the Defense Advanced +Research Projects Agency, and the Army Research Office (ARO) under +contract no. DAAD19-01-1-0485, and the General Motors +Collaborative Research Lab at CMU. The views and conclusions +contained in this document are those of the author and should not +be interpreted as representing the official policies, either +expressed or implied, of SRC, NSF, ONR, NRL, DOD, ARO, or the U.S. +government. |