 |
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, 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 You should also read the license. |  |
NEW: Version 3.0 released.
NEW: We are hiring PhD students and Postdocs at Oxford University.
 |
 |
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.
The following papers describe interesting applications of CBMC:
This paper describes a modified version of CBMC
that can find the cause of an error.
CBMC is used to localize the possible cause of a fault.
This paper describes a
version of CBMC for concurrent software.
This
paper describes an application of CBMC to the verification of Linux
Device Drivers.
This paper describes an algorithm to show equivalence of two
programs. The resulting verification condition is discharged with
CBMC.
This paper describes an application of CBMC to finding security-relevant
bugs in WIN32 binaries.
This paper describes an application of CBMC to test-vector generation.
An application of CBMC for test-vector generation.
An application of CBMC to filter warnings generated by
PolySpace.
CBMC is used to verify multiple configurations of a program
simultaneously.
An application of CBMC and SATABS to a medical device.
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-0-win.zip
Unzip the archive before running. You will need CL (comes with Visual C) in your PATH for preprocessing.CBMC for Linux/x86: cbmc-3-0-linux.tgz
Dotar xfz cbmc-3-0-linux.tgzbefore running. It is linked statically to avoid trouble with libraries. A 64-bit version is here.CBMC for MacOS (universal): CBMC-3.0.dmg
The binary is installed in /usr/local/bin.ANSI-C Headers: ansi-c-lib.tgz
Dotar xfz ansi-c-lib.tgzto unpack.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.
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.