We are pleased to announce the release of CBMC version 4.3.
This release adds a range of new features.
* IEEE floating-point arithmetic now takes the rounding mode into account, which can be changed dynamically.
* goto-gcc generates hybrid executables on Linux, containing both machine code and the CFG for CBMC/SATABS.
* Limited support for Spec#-style quantifiers added.
* Pointer-checks no longer use a heavy-weight alias analysis.
* Limited support for some x86, Power and ARM inline assembly constructs.
* Extended support for Z3 and Boolector (using the SMT1 file interface) and MathSAT (using the SMT2 file interface)
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 .deb packages above once these are stable releases).
The version of goto-instrument shipped with CBMC 4.3 supports the instrumentation of programs for the weak memory consistency models of Intel's x86, RMO, TSO, Power and ARM. Details can be found in our upcoming ESOP 2013 paper: