JBMC is a Bounded Model Checker for Java programs. It supports checking for runtime exceptions and user-defined assertions. The verification is performed by unwinding the loops in the program and passing the resulting equation to a decision procedure.

More info...

Get the latest release

• Releases are tested and for production use.

Get the current develop version: git clone https://github.com/diffblue/cbmc.git

• Develop versions are not recommended for production use.

JBMC compiles CBMC as part of its build process and as such has all the pre-requisites of CBMC. These can be viewed at: diffblue/cbmc:COMPILING

Before compilation, run the commands:

make -C src DOWNLOADER=wget minisat2-download
make -C jbmc/src setup-submodules

Then compile using:

make -C jbmc/src

Compiling produces an executable called jbmc which by default can be found in jbmc/src/jbmc/jbmc

See CBMC)

4-clause BSD license, see LICENSE file.