JJBMC

JJBMC is a tool that is developed both at FZI and KIT, which enables the software bounded model checker JBMC to verify contracts written in the Java Modeling Language (JML). In order to run the tool, you have 3 options:

Build it manually.
Use our prebuilt docker image (notice, however, that proofs will take significantly longer in the docker version and this may not always be up to date).
Use the prebuilt version (development version).

Using the Docker Image

Install docker if you do not have it already installed (e.g., via sudo curl -sSL https://get.docker.com/ | sh).
For the following step, you might need to prefix the call with sudo if you are not a member of the docker group.
Run the interactive container via docker run -it jonasklamroth/jjbmc.
Run JJBMC as shown below in the section Running JJBMC.

Building JJBMC Manually

Requirements

Java 8 (both newer and older versions do not work due to incompatibilities with OpenJML)
Gradle 6.4.1 or higher (only if gradle wrapper does not work on your system)
Preferably some Unix OS (tested only on Ubuntu 20.04)

Compiling JJBMC

Make sure that JAVA_HOME points to a valid installation of Java 8 (tested for openjdk).
Checkout the source code via git clone git@github.com:JonasKlamroth/JJBMC.git (for a checkout using SSH).
Build the jar file via ./gradlew fatJar (JJBMC.jar will appear in the root folder of your project).
If the previous step does not work, first create a gradle wrapper via gradle wrapper.

Running JJBMC

Important: JJBMC uses JBMC as a backend. Please make sure that a recent version (currently >= 5.22) of JBMC is installed and included in the path. To download and install the latest JBMC version (as part of CBMC) go to https://github.com/diffblue/cbmc/releases/.
You can see the available command-line options via java -jar JJBMC.jar.
In general, you can run JJBMC via java -jar JJBMC.jar JAVA_FILE METHOD_NAME -j="JBMC_OPTIONS", where JAVA_FILE should be replaced by the JML-specified Java file that you want to analyze, METHOD_NAME can be replaced by a name of a method you would like to verify (if left out all methods are verified), and JBMC_OPTIONS should be replaced by the JBMC options that you want to set, e.g., a bound for loop unrollings via --unwind BOUND (BOUND should be replaced by the size of the desired bound). For examples, see the section below.

Examples

You can analyze a correct modular Bubblesort example via

java -jar JJBMC.jar testRes/BubbleSort.java sort

You can analyze the same Bubblesort example, however with a wrong specification via

java -jar JJBMC.jar testRes/BubbleSort.java broken_sort

You can analyze force a non modular verification (inlining all loop invariants and methods) of the [Bubblesort example](testRes/BubbleSort.java](https://github.com/JonasKlamroth/JJBMC/blob/master/testRes/CaseStudy/BubbleSort.java) via

java -jar JJBMC.jar testRes/BubbleSort.java -fi

You can analyze the Hammingweight example via

java -jar JJBMC.jar testRes/NormalHammingWeight.java -u 33

Publications

Publication introducing JJBMC:

Bernhard Beckert, Michael Kirsten, Jonas Klamroth, and Mattias Ulbrich: Modular Verification of JML Contracts Using Bounded Model Checking. (in proceedings of ISOLA 2020)

Publications of research in which JJBMC was used:

Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, and Alexander Weigl: Formal Specification and Verification of JDK’s Identity Hash Map Implementation (in proceedings of iFM 2022)
Jonas Klamroth, Florian Lanzinger, Wolfram Pfeifer, and Mattias Ulbrich: The Karlsruhe Java Verification Suite (In The Logic of Software, Springer, 2022)

wadoon/JJBMC