The CBMC Homepage

Bounded Model Checking
for ANSI-C

chip CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Furthermore, it can check ANSI-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.

While CBMC is aimed for embedded software, it also supports dynamic memory allocation using malloc and new. For questions about CBMC, contact Daniel Kroening.

You should also read the CBMC license.

CBMC has featured support for SMT solvers since version 3.3. The solvers we recommend are (in no particular order) Boolector, MathSAT and Z3. Note that these solvers need to be installed separately and have different licensing conditions.

NEW: CPROVER Visual Studio plugin released.

NEW: Version 4.3 released.

Version 3.3.2 for Linux/Windows/Mac released.
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.
A set of slides on CBMC: PDF, 2x3 handouts.
The sources are available here.
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.

Windows	Command Line Download cbmc-4-3-win.zip, and then unzip the archive. You will need to run CBMC from the Visual Studio Command Prompt. The free Visual C++ 2010 Express is sufficient.
Linux	If you have Debian Wheezy or later, or a recent Ubuntu distribution, then install the package cbmc with `apt-get install cbmc` 32-bit Linux/i386: cbmc-4-3-linux-32.tgz 64-bit Linux/x64: cbmc-4-3-linux-64.tgz Do `tar xfz cbmc-4-3-linux-32.tgz` before running. CBMC for Debian/i386: cbmc_4.3_i386.deb CBMC for Debian/AMD64: cbmc_4.3_amd64.deb Install with `dpgk -i filename`
MacOS	CBMC for MacOS (Intel 64 only): cbmc-4-3.pkg The binary is installed in /usr/bin. You need to have the Command Line Tools for Xcode, which can be downloaded here.
Source Code	Source code is available via `svn co http://www.cprover.org/svn/cbmc/releases/cbmc-4.3`

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.