C Bounded Model Checker
Switch branches/tags
Clone or download
tautschnig Merge pull request #2897 from danpoe/refactor/error-handling-cleanup-…

Error handling cleanup in solvers/flattening
Latest commit f7e224b Sep 25, 2018
Failed to load latest commit information.
.githooks Make the pre-commit hook report non-temporary path names (#477) Feb 2, 2017
.github Merge pull request #2972 from tautschnig/issue-template Sep 19, 2018
cmake Add DownloadProject cmake script Sep 27, 2017
doc Merge pull request #2806 from johanneskloos/doc-background-section Sep 24, 2018
jbmc Merge pull request #3035 from tautschnig/address_mapt Sep 24, 2018
pkg/arch Add CBMC package build file for Arch Linux Apr 26, 2017
regression Merge pull request #3023 from diffblue/quantifier-op-type Sep 24, 2018
scripts ls_parse: improve debugging by printing a trace Jul 12, 2018
src Merge pull request #2897 from danpoe/refactor/error-handling-cleanup-… Sep 25, 2018
unit Merge pull request #3030 from tautschnig/format-number-range Sep 24, 2018
.clang-format Sort includes using clang-format Apr 23, 2018
.dir-locals.el Move Emacs style file so it affects unit tests as well as main source Aug 16, 2017
.editorconfig Don't remove trailing spaces from patch files Nov 29, 2016
.gitattributes added test.desc as text Aug 15, 2016
.gitignore use a string instead of macro for version number Jul 31, 2018
.gitmodules Use submodule to download java-models-library Jul 9, 2018
.travis.yml Workaround for Google Cloud SDK packaging problem Sep 19, 2018
CHANGELOG Add new goto-instrument option print-global-state-size Jun 20, 2018
CMakeLists.txt Make the remaining (relevant) miniBDD catch-style unit tests Sep 18, 2018
CODEOWNERS Remove code owners from low-risk files Jul 24, 2018
CODING_STANDARD.md State that identifiers should be good Aug 10, 2018
COMPILING.md Document the IPASIR build in a single place Sep 19, 2018
LICENSE update year Sep 5, 2016
README.md Add AWS CodeBuild badges Aug 15, 2018
buildspec-windows.yml CodeBuild: Remove empty artifact stanza Aug 11, 2018
buildspec.yml CodeBuild: Remove empty artifact stanza Aug 11, 2018
gcloud-travis-cbmc.json.enc Add encrypted GCloud key for Travis Mar 20, 2018


Build Status Build Status Build Status Build Status

CProver Wiki

CProver Documentation


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, exceptions and user-specified assertions. 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 resulting equation to a decision procedure.

For full information see cprover.org.


Get the latest release

  • Releases are tested and for production use.

Get the current develop version: git clone https://github.com/diffblue/cbmc.git

  • Develop versions are not recommended for production use.

Report bugs

If you encounter a problem please file a bug report:

Contributing to the code base

  1. Fork the repository
  2. Clone the repository git clone git@github.com:YOURNAME/cbmc.git
  3. Create a branch from the develop branch (default branch)
  4. Make your changes (follow the coding guidelines)
  5. Push your changes to your branch
  6. Create a Pull Request targeting the develop branch


4-clause BSD license, see LICENSE file.