![]() |
Bounded Model Checking for ANSI-C |
|

CBMC is a Bounded Model
Checker for ANSI-C and C++ programs. 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. This is done 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 license.

NEW: Version 3.6 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.

From a user's point of view, the CBMC manual gives a tutorial and describes what properties are checked. We also have two papers that describe how to use CBMC for hardware verification.
- Supported Language Features
- CBMC Manual (PDF) (updated, also covers SATABS)
- 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 and Windows
for CBMC itself, 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.
CBMC for Windows: cbmc-3-6-win.zip
Unzip the archive before running. You will need CL (comes with Microsoft Visual Studio) in your PATH for preprocessing.CBMC for Linux/i386: cbmc-3-6-linux.tgz
Dotar xfz cbmc-3-6-linux.tgzbefore running. It is linked statically to avoid trouble with libraries.CBMC for Debian/i386: cbmc_3.6_i386.deb
Install withdpgk -i cbmc_3.6_i386.debCBMC for MacOS (universal): cbmc-3-6-mac.mpkg.zip
The binary is installed in /usr/bin.Installation instructions for the Eclipse Plugin
Source: cbmc-2-4-p1-src.tgz
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.



