CBMC Release 5.2

[Daniel Kroening]

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

This is a minor release, focused primarily on maintenance. The primary
areas of attention are the full slicer, the Java frontend, test suite
generation and support for the Glucose solver.

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

* Linux:
http://www.cprover.org/cbmc/download/cbmc-5-2-linux-32.tgz
http://www.cprover.org/cbmc/download/cbmc-5-2-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-2-win.zip

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

The source code is available via SVN at
http://www.cprover.org/svn/cbmc/releases/cbmc-5.2. From source, binaries
for FreeBSD 10 and Solaris 11 can be built. Note that version 5.2 will
be the last version of CBMC to build with pre-C++11 compilers.

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:

* Synthesising Interprocedural Bit-Precise Termination Proofs
http://www.kroening.com/papers/ase2015.pdf

* From AgentSpeak to C for Safety Considerations in Unmanned Aerial Vehicles
http://dx.doi.org/10.1007/978-3-319-22416-9_9

* Hardware Verification using Software Analyzers
http://www.kroening.com/papers/ISVLSI2015-1.pdf

* Equivalence Checking using Trace Partitioning
http://www.kroening.com/papers/ISVLSI2015-2.pdf

* Successful Use of Incremental BMC in the Automotive Industry
http://dx.doi.org/10.1007/978-3-319-19458-5_5

* On Partial Order Semantics for SAT/SMT-based Symbolic Encodings of
Weak Memory Concurrency
http://www.kroening.com/papers/forte2015-wm.pdf

Daniel