CBMC Release 5.1

[Daniel Kroening]

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

This is a minor release, focused primarily on maintenance. Support for solving floating-point problems using for SMT-LIB2 solvers without support for the floating-point theory has been added.

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

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

Recall that CBMC packages come with Debian, Ubuntu, and Fedora.

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

* MacOS X binary for 64 bit Intel for OS X 10.6 or higher:
http://www.cprover.org/cbmc/download/cbmc-5-1.pkg

The source code is available via SVN at http://www.cprover.org/svn/cbmc/releases/cbmc-5.1. From source, binaries for FreeBSD 10 and Solaris 11 can be built.

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

* Under-Approximating Loops in C Programs for Fast Counterexample Detection
http://dx.doi.org/10.1007/s10703-015-0228-1

* Proving Safety with Trace Automata and Bounded Model Checking
http://www.kroening.com/papers/fm2015-trace-automata.pdf

* Property-Driven Fence Insertion using Reorder Bounded Model Checking
http://www.kroening.com/papers/fm2015-robmc.pdf

* Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs
http://link.springer.com/chapter/10.1007%2F978-3-662-46669-8_27

* Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
http://link.springer.com/chapter/10.1007%2F978-3-662-46669-8_8

* Effective Verification of Low-Level Software with Nested Interrupts
http://www.kroening.com/papers/date2015.pdf

Daniel