JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode

About JBMC

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

For questions about JBMC, con­tact Peter Schrammel. You should also read the license (4-clause BSD).

JBMC News

A JBMC tool paper has been accepted at CAV 2018.

There is a Google Group for annoucements related to JBMC.

 

JBMC Documentation

We provide a two minute guide how to use JBMC.

Let us consider the following Java program (Simple.java): 

    
 1. package my.petty.examples;
 2.
 3. public class Simple {
 4.
 5.     public static void main(String[] args) {
 6.         String s = new String("Abc");
 7.         String u = "bc";
 8.         assert(!s.contains(u)); // This assert failure should be found by JBMC!
 9.     }                           
10.
11. }

saved into a file <some-directory>/my/petty/examples/Simple.java. First, we need to compile the class file as follows: 

    
<some-directory>$ javac my/petty/examples/Simple.java

This command creates a class file <some-directory>/my/petty/examples/Simple.class. We are now ready to use JBMC to check for defects in our program. We do so by executing the following command in the directory <some-directory>: 

    
<some-directory>$ <path-to-jbmc>/jbmc my.petty.examples.Simple --unwind 5 --classpath <path-to-jbmc>/core-models.jar:.

NOTE: The user needs to run the above command in the directory <some-directory> since JBMC uses a similar strategy as JVM when searching for class files. The core-models.jar contains JBMC's model of the Java runtime library.

Here is the last part of the output produced by JBMC 5.12: 


my/petty/examples/Simple.java function java::my.petty.examples.Simple.main:([Ljava/lang/String;)V
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.1] line 6 no uncaught exception: SUCCESS
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 6 Null pointer check: SUCCESS
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.assertion.1] line 8 assertion at file my/petty/examples/Simple.java line 8 function java::my.petty.examples.Simple.main:([Ljava/lang/String;)V bytecode-index 16: FAILURE
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.null-pointer-exception.2] line 8 Null pointer check: SUCCESS
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.null-pointer-exception.3] line 8 Null pointer check: SUCCESS

** 1 of 47 failed (2 iterations)
VERIFICATION FAILED

The result 'VERIFICATION FAILED' indicates that JBMC has found a defect in the program. In order to locate the defect we look for 'FAILURE' in the list of results. We see that the defect is in line 8 in our Java file.

JBMC provides many command line options for customizing the analysis. The options are listed here. You can also get a list by using the option --help.

 

JBMC Download

The development version of the JBMC sources can be downloaded from the github repository.

CAV'18 Experiments

We provide all resources required for reproducing the results reported in our CAV 2018 tool paper.