CBMC Release 4.3

[Daniel Kroening]

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

This release adds a range of new features.

* IEEE floating-point arithmetic now takes the rounding mode into account, which can be changed dynamically.

* goto-gcc generates hybrid executables on Linux, containing both machine code and the CFG for CBMC/SATABS.

* Limited support for Spec#-style quantifiers added.

* Pointer-checks no longer use a heavy-weight alias analysis.

* Limited support for some x86, Power and ARM inline assembly constructs.

* Extended support for Z3 and Boolector (using the SMT1 file interface) and MathSAT (using the SMT2 file interface)

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

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

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

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

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

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

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.

The version of goto-instrument shipped with CBMC 4.3 supports the instrumentation of programs for the weak memory consistency models of Intel's x86, RMO, TSO, Power and ARM. Details can be found in our upcoming ESOP 2013 paper:

http://www.kroening.com/publications/view-publications-aknt2013-esop.html