CBMC Release 4.4

[Daniel Kroening]

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

This release adds a major range of new features.

* CBMC now supports checking concurrent programs, using pthreads or the WIN32 thread APIs. Details can be found in the following upcoming CAV 2013 paper:

http://www.kroening.com/publications/view-publications-akt2013-cav.html

* Support for the proposed standard SMT-LIB Floating-point theory.

* goto-instrument supports k-induction and under-approximative loop acceleration. Details on the loop acceleration can be found in the following upcoming CAV 2013 paper:

http://www.kroening.com/publications/view-publications-klw2013-cav.html

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

* Linux:
http://www.cprover.org/cbmc/download/cbmc-4-4-linux-32.tgz 
http://www.cprover.org/cbmc/download/cbmc-4-4-linux-64.tgz

Note that newer releases of Debian and Ubuntu include a package for CBMC, which can be installed via apt-get. Fedora also has a CBMC package.

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

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

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

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.