|Bounded Model Checking|
CBMC is a Bounded
Model Checker for C and C++ programs. It supports C89, C99, most of C11 and
most compiler extensions provided by gcc and Visual Studio. A variant
of CBMC that analyses Java bytecode is available as
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 consistency 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 is available for most flavours of Linux (pre-packaged on
Debian, Ubuntu and Fedora), Solaris 11, Windows and MacOS X.
You should also read the
For questions about
CBMC, contact Daniel Kroening.
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, MathSAT, Yices 2 and Z3. Note that these solvers need to be installed separately and have different licensing conditions.
NEW: Eclipse Plugin redesigned!
NEW: Version 5.11 released.
There is a Google Group for annoucements related to CBMC.
The CPROVER Manual contains a tutorial from a user's point of view and describes what properties are checked.
- The primary reference for CBMC is A Tool for Checking ANSI-C Programs (ca. 1300 citations).
We also have a list of interesting applications of CBMC.
We are releasing binaries for x86 Linux, Windows, and MacOS.
Installation instructions for the Eclipse Plugin
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.