We are pleased to announce the release of CBMC version 4.4.
This release adds a major range of new features.
* CBMC now supports checking concurrent programs, using pthreads or the WIN32 thread APIs. Details can be found in the following upcoming CAV 2013 paper:
* Support for the proposed standard SMT-LIB Floating-point theory.
* goto-instrument supports k-induction and under-approximative loop acceleration. Details on the loop acceleration can be found in the following upcoming CAV 2013 paper:
Note that newer releases of Debian and Ubuntu include a package for CBMC, which can be installed via apt-get. Fedora also has a CBMC package.