CBMC Release 4.1

[Daniel Kroening]

We are pleased to announce the release of CBMC version 4.1.

This is again mostly a maintenance release, which fixes problems of the previous versions. The support for low-level accesses to dynamically allocated data structures and "integer addressed memory" (usually memory-mapped I/O) has been further improved.

The release also includes numerous improvements to the SMT back-ends. Specifically, support through the SMT1 path for Boolector and Z3 has been improved; support for MathSAT has been added. In combination with the very latest version of MathSAT, CBMC now also supports an SMT2 flow (use --mathsat --smt2 to activate this).

Both CBMC 4.1 and HW-CBMC 4.1 are available in binary form at http://www.cprover.org/cbmc/ for the following architectures: 

* Linux:
http://www.cprover.org/cbmc/download/cbmc-4-1-linux-32.tgz 
http://www.cprover.org/cbmc/download/cbmc-4-1-linux-64.tgz
http://www.cprover.org/cbmc/download/cbmc_4.1_i386.deb
http://www.cprover.org/cbmc/download/cbmc_4.1_amd64.deb

Debian unstable and newer variants of Ubuntu include a package for CBMC, which can be installed via apt-get (we will therefore discontinue the distribution of the binary packages above once these are stable releases).

* Windows (32 bit):
http://www.cprover.org/cbmc/download/cbmc-4-1-win.zip 

* MacOS X fat binary for 32 and 64 bit Intel:
http://www.cprover.org/cbmc/download/cbmc-4-1.pkg

The source code is available via SVN at http://www.cprover.org/svn/cbmc/releases/cbmc-4.1.

The packages also include goto-cc and goto-instrument. The goto-instrument program contains new features, which are primarily aimed at embedded software:

 --nondet-volatile -- makes reads from volatile variables non-deterministic

 --isr function -- instruments an interrupt service routine

 --nondet-static -- add nondeterministic initialization of variables with static lifetime

As a reminder, 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 paper:

Software Verification Using k-Induction

The paper describes a variant of BMC that can prove properties for unbounded loops.
http://www.kroening.com/publications/view-publications-dhkr2011-sas.html