|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. It also
using Scoot. It allows verifying array bounds (buffer
overflows), pointer safety, exceptions 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 aimed for embedded software, it also supports
dynamic memory allocation using
For questions about
CBMC, contact Daniel Kroening.
CBMC is available for most flavours of Linux (pre-packaged on
Debian and Fedora), Solaris 11, Windows and MacOS X.
You should also read the
CBMC has featured support for SMT solvers since version 3.3. The solvers we recommend are (in no particular order) Yices 2, MathSAT and Z3. The Boolector solver currently lacks support for model generation when using the SMT 2 interface. Note that these solvers need to be installed separately and have different licensing conditions.
NEW: CPROVER Visual Studio plugin released.
NEW: Version 5.0 released.
Version 3.3.2 for
This comes with preliminary support for SMT version 2.
Version 3.3.1 for Windows released.
This version fixes a problem with preprocessing, and includes Minisat 2.
Version 3.3 released.
This version has premilinary support for Boolector, CVC3, Yices, and Z3 via the SMT-Lib theory QF_AUFBV.
NEW: There is now a Google Group for annoucements related to CBMC.
Click to enlarge.
The CPROVER Manual gives a tutorial from a user's point of view and describes what properties are checked.
- Hardware Verification using ANSI-C Programs as a Reference
- Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
- A Tool for Checking ANSI-C Programs
We also have a list of interesting applications of CBMC.
We are releasing binaries for x86 Linux, Windows,
and MacOS, the source code, and the Eclipse Plugin. The current
version supports the following file formats: ANSI-C, C++, SMV, Verilog, and
netlists. Note that there are two executables:
cbmc for ANSI-C
verification only, and
hw-cbmc, which supports Verilog as
well. We are currently preparing a release
with support for SpecC and SystemC.
Installation instructions for the Eclipse Plugin
If you need a Model Checker for Verilog or SMV files, consider EBMC.
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.
This research is currently supported by EPSRC grant EP/H017585/1.