CBMC Release 4.0

105 views
Skip to first unread message

Daniel Kroening

unread,
Jun 14, 2011, 2:53:14 PM6/14/11
to cpr...@googlegroups.com
We are pleased to announce the release of CBMC version 4.0.

This is again mostly a maintenance release, which fixes problems of the previous versions. The main emphasis has been better support for low-level accesses to dynamically allocated data structures. The release also includes numerous front-end improvements.

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

* Linux:
http://www.cprover.org/cbmc/download/cbmc-4-0-linux-32.tgz
http://www.cprover.org/cbmc/download/cbmc-4-0-linux-64.tgz
http://www.cprover.org/cbmc/download/cbmc_4.0_i386.deb
http://www.cprover.org/cbmc/download/cbmc_4.0_amd64.deb

Debian unstable includes a package for CBMC, which can be installed via apt-get (we will therefore eventually discontinue the distribution of the binary packages above).

* Windows:
http://www.cprover.org/cbmc/download/cbmc-4-0-win.zip

* MacOS X 64 bit Intel:
http://www.cprover.org/cbmc/download/cbmc-4-0.pkg

The source code is available via SVN at http://www.cprover.org/svn/cbmc/releases/cbmc-4.0.

The new 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 related papers:

1) Automatic Analysis of DMA Races Using Model Checking and k-induction
The paper describes a variant of BMC that can prove properties for unbounded loops.
http://www.kroening.com/publications/view-publications-dkr2011-fmsd.html

2) Test-Case Generation for Embedded Simulink via Formal Concept Analysis
The paper describes an application of CBMC to test-vector generation for Simulink.
http://www.kroening.com/publications/view-publications-hrk2011-dac.html

Reply all
Reply to author
Forward
0 new messages