All groups and messages
Send feedback to Google
The CProver Group
CBMC Release 5.1
Skip to first unread message
May 10, 2015, 3:38:03 PM
Reply to author
Sign in to reply to author
Sign in to forward
Report message as abuse
Sign in to report message as abuse
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
We are pleased to announce the release of CBMC version 5.1.
This is a minor release, focused primarily on maintenance. Support for solving floating-point problems using for SMT-LIB2 solvers without support for the floating-point theory has been added.
Both CBMC 5.1 and HW-CBMC 5.1 are available in binary form at
for the following architectures:
Recall that CBMC packages come with Debian, Ubuntu, and Fedora.
* Windows (32 bit and 64 bit):
* MacOS X binary for 64 bit Intel for OS X 10.6 or higher:
The source code is available via SVN at
. From source, binaries for FreeBSD 10 and Solaris 11 can be built.
As a reminder, the HTML-based manual is available at:
The manual not only covers CBMC, but also HW-CBMC and SATABS.
You may also be interested in the following papers:
* Under-Approximating Loops in C Programs for Fast Counterexample Detection
* Proving Safety with Trace Automata and Bounded Model Checking
* Property-Driven Fence Insertion using Reorder Bounded Model Checking
* Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs
* Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
* Effective Verification of Low-Level Software with Nested Interrupts
Reply to author
0 new messages