CBMC Homepage Bounded Model Checking
for Software


About CBMC

chip 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 supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions and user-specified as­ser­tions. 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 re­sul­ting 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.

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 license.

CBMC comes with a built-in solver for bit-vector formulas that is based on MiniSat. As an alternative, CBMC has featured support for external SMT solvers since version 3.3. The solvers we recommend are (in no particular order) Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be installed separately and have different licensing conditions.



NEW: Eclipse Plugin redesigned!

NEW: Version 5.2 released.

There is a Google Group for annoucements related to CBMC.


CBMC Documentation

We also have a list of interesting applications of CBMC.


CBMC Download

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.


Command Line

Download, and then unzip the archive. You will need to run CBMC from the Visual Studio Command Prompt. We recommend you install the free Visual Studio Community.

CPROVER Visual Studio plugin


If you have Debian Wheezy or later, or a recent Ubuntu distribution, then install the package cbmc with apt-get install cbmc

On Fedora 18 or newer, do yum install cbmc

Otherwise, download one of the following binaries:
32-bit Linux/i386: cbmc-5-2-linux-32.tgz
64-bit Linux/x64: cbmc-5-2-linux-64.tgz
Do tar xfz cbmc-5-2-linux-32.tgz before running.


CBMC for MacOS (Intel 64 binary): cbmc-5-2.pkg
OS X 10.6 or higher is required. 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

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.