CBMC Release 5.7

[Daniel Kroening]

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

This is a major release, with numerous changes. The key emphasis have
been improvements to the Java frontend.

Note that the option --conversion-check is now required to catch type
casts that cause loss of information. Previously,
--(un)signed-overflow-check would report these.

CBMC 5.7 is available in binary form at http://www.cprover.org/cbmc/ for
the following architectures:

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

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

* Windows (64 bit only):
http://www.cprover.org/cbmc/download/cbmc-5-7-win.zip

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

The source code is available on GitHub.

From source, binaries for FreeBSD and Solaris can be built. Note
that CBMC has required a C++11 compiler since version 5.3.

As a reminder, the HTML-based manual is available at:

http://www.cprover.org/cprover-manual/

You may also be interested in the following papers:

* Sound and Automated Synthesis of Digital Stabilizing Controllers for
Continuous Plants
http://www.kroening.com/papers/hscc2017.pdf

* Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence
Insertion
http://www.kroening.com/papers/toplas2017-musketeer.pdf

* Equivalence Checking of a Floating-point Unit Against a High-level C Model
http://www.kroening.com/papers/fm2016-float.pdf

* Assisted Coverage Closure
http://www.kroening.com/papers/nfm2016.pdf

With best regards,

Daniel