CBMC Homepage

Bounded Model Checking for ANSI-C

About CBMC

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 SAT solver.

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.

CBMC News

NEW: Version 2.8 released. There are two executables: cbmc for ANSI-C verification only, and hw-cbmc, which supports Verilog as well.

We are releasing binaries for x86 Linux and Windows for CBMC itself, and the Eclipse Plugin. The current version supports the following file formats: ANSI-C, C++, SMV, Verilog, and netlists.

We are currently preparing a release with support for SpecC and SystemC.

NEW: ECLIPSE Plugin for CBMC

CBMC Screenshots

CBMC Documentation

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)
Hardware Verification using ANSI-C Programs as a Reference
Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
Error Explanation with Distance Metrics
This paper describes a modified version of CBMC that can find the cause of an error.
A Tool for Checking ANSI-C Programs

CBMC Download

We distribute binaries for x86 Linux and Windows, and the source code.

CBMC for Windows: cbmc-2-8-win.zip
Unzip the archive before running. You will need CL (comes with Visual C) in your PATH for preprocessing.

cbmc-2-8-linux.tgz

tar xfz cbmc-2-8-linux.tgz

ANSI-C Headers: ansi-c-lib.tgz
Do tar xfz ansi-c-lib.tgz to unpack.
Installation instructions for the Eclipse Plugin
Source: cbmc-2-4-src.tgz

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.