CBMC

About CBMC

CBMC is a Bounded Model Checker for C and C++ programs. It sup­ports C89, C99, most of C11/C17 and most compi­ler exten­sions pro­vided by gcc, clang, and Visual Studio. A variant of CBMC that analyses Java bytecode is available as JBMC. For Rust, get Kani.

CBMC verifies memory safety (which includes array bounds checks and checks for the safe use of pointers), checks for various further variants of undefined behavior, and user-specified as­ser­tions. Further­more, it can check C and C++ for I/O equivalence 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.

CBMC is available for most flavours of Linux (pre-packaged for Debian/Ubuntu), Windows and MacOS. You should also read the CBMC license (BSD 4-clause).

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, CVC5 and Z3. Note that these solvers need to be installed separately and have different licensing conditions.

For questions about CBMC, contact Daniel Kroening.

CBMC News

CBMC version 6 has been released!

Major changes:

• Checks for undefined behavior are now on by default. Use --no-standard-checks to restore the previous default.
• The default behavior of malloc now enables returning NULL. Use --no-malloc-may-fail to restore the previous default.
• Calls to functions without body now trigger a verification error.
• The default verbosity is now 6. Use --verbosity 8 to restore the previous default.

CBMC Documentation

• The CPROVER Manual contains 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.

• The primary reference for CBMC is A Tool for Checking ANSI-C Programs (ca. 1900 citations).

We also have a list of interesting applications of CBMC.

CBMC Download

We are maintaining CBMC for x86 Linux, Windows and MacOS.

Windows	Download cbmc-6.1.0-win64.msi, and then double-click to install. This is an x64 binary for the command line (there is no GUI). You will need to run CBMC from the Visual Studio Command Prompt. We recommend you install the free Visual Studio Community.
Ubuntu 24.04 and Debian trixie	Do     apt-get install cbmc to install. This will give you cbmc 6.0.1.
Debian   Ubuntu 20.04 and 22.04	While the current stable Debian and Ubuntu 20/22.04 do have a cbmc package, this package is at version 5.12, which is more than a decade old. Download one of the following binary packages: 64-bit Ubuntu 20.04/x64: ubuntu-20.04-cbmc-6.1.0-Linux.deb 64-bit Ubuntu 22.04/x64: ubuntu-22.04-cbmc-6.1.0-Linux.deb Do     dpkg -i ubuntu-20.04-cbmc-6.1.0-Linux.deb to install.
Fedora	On Fedora 18 or newer, you can do     yum install cbmc This will give you version 5.50.
MacOS	To get a recent version of CBMC, consider using Homebrew, and then do     brew install cbmc This is a command-line tool only, there is no GUI. You need to have the Command Line Tools for Xcode, which can be downloaded by running the Xcode application or from here.
Source Code	Source code is available here.

If you need a Model Checker for Verilog or SystemVerilog, 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.