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, ex­cep­tions 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 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.

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
  Do tar xfz cbmc-3-6-linux.tgz before running. It is linked statically to avoid trouble with libraries.

  CBMC for Debian/i386: cbmc_3.6_i386.deb
  Install with dpgk -i cbmc_3.6_i386.deb

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