CBMC Release 4.2

[Daniel Kroening]

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

This release adds a range of new features.

* goto-cc now passes all command line options to the gcc preprocessor, and is able to read the goto-binary portion from an ELF object file.

  

* The MacOS binaries are now signed.

* The C/C++ front-end has been tested and fixed for the Visual Studio 2012 header files.

* The man-page has been elaborated.

* Support for the C99 complex type and gcc's vector type has been added. Various built-ins for x86 MMX and SSE instructions have been added.

* Support for various C11 features has been added, including unicode string and character literals and _Generic.

* Support for various built-in primitives has been added, in particular for the __sync_* commands.

* New feature: --all-claims now reports the status of all claims; the verification continues even if a counterexample is found. This feature uses incremental SAT.

* New feature: --cover-assertions checks whether all assertions are reachable, and reports those that are not.

* The counterexample beautification (--beautify) now uses incremental SAT.

* Numerous improvements to SMT1 and SMT2 interfaces.

* Support for further SAT solvers (PRECOSAT, PICOSAT, LINGELING)

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

* Linux:
http://www.cprover.org/cbmc/download/cbmc-4-2-linux-32.tgz 
http://www.cprover.org/cbmc/download/cbmc-4-2-linux-64.tgz
http://www.cprover.org/cbmc/download/cbmc_4.2_i386.deb
http://www.cprover.org/cbmc/download/cbmc_4.2_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 packages above once these are stable releases).

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

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

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

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:

Numeric Bounds Analysis with Conflict-Driven Learning

The paper describes a variant of CBMC that uses a novel technique for verifying properties of programs that use IEEE floating-point arithmetic.

http://www.kroening.com/publications/view-publications-dhkt2012.html