CBMC Release 4.0
Daniel Kroening
This is again mostly a maintenance release, which fixes problems of the previous versions. The main emphasis has been better support for low-level accesses to dynamically allocated data structures. The release also includes numerous front-end improvements.
Both CBMC 4.0 and HW-CBMC 4.0 are available in binary form at http://www.cprover.org/cbmc/ for the following architectures:
* Linux:
http://www.cprover.org/cbmc/download/cbmc-4-0-linux-32.tgz
http://www.cprover.org/cbmc/download/cbmc-4-0-linux-64.tgz
http://www.cprover.org/cbmc/download/cbmc_4.0_i386.deb
http://www.cprover.org/cbmc/download/cbmc_4.0_amd64.deb
Debian unstable includes a package for CBMC, which can be installed via apt-get (we will therefore eventually discontinue the distribution of the binary packages above).
* Windows:
http://www.cprover.org/cbmc/download/cbmc-4-0-win.zip
* MacOS X 64 bit Intel:
http://www.cprover.org/cbmc/download/cbmc-4-0.pkg
The source code is available via SVN at http://www.cprover.org/svn/cbmc/releases/cbmc-4.0.
The new HTML-based manual is available at:
http://www.cprover.org/cprover-manual/
The manual not only covers CBMC, but also HW-CBMC and SATABS.
You may also be interested in the following related papers:
1) Automatic Analysis of DMA Races Using Model Checking and k-induction
The paper describes a variant of BMC that can prove properties for unbounded loops.
http://www.kroening.com/publications/view-publications-dkr2011-fmsd.html
2) Test-Case Generation for Embedded Simulink via Formal Concept Analysis
The paper describes an application of CBMC to test-vector generation for Simulink.
http://www.kroening.com/publications/view-publications-hrk2011-dac.html