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.

 

CBMC Download


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

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.