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:
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).
* MacOS X 64 bit Intel:
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:
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.
2) Test-Case Generation for Embedded Simulink via Formal Concept Analysis
The paper describes an application of CBMC to test-vector generation for Simulink.