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.

JBMC News

A JBMC tool paper has been accepted at CAV 2018.

There is a Google Group for annoucements related to JBMC.

 

JBMC Documentation

The CPROVER Manual gives a tutorial from a user's point of view and describes what properties are checked.

Here we provide a 2 minutes guide how to use JBMC.

Let us consider the following Java program:

    
 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>/Simple.java. First, we need to compile the class file as follows:

    
<some-directory>$ javac Simple.java -d .
    

This command creates a class file <some-directory>/my/petty/examples/Simple.class. We are 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.class  --unwind 5
    

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.

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

    
** Results:
[java::my.petty.examples.Simple.<init>:()V.null-pointer-exception.1] Throw null: SUCCESS
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.null-pointer-exception.1] Throw null: SUCCESS
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.null-pointer-exception.2] Throw null: SUCCESS
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.null-pointer-exception.3] Throw null: SUCCESS
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.assertion.1] assertion at file my/petty/examples/Simple.java line 8
        function java::my.petty.examples.Simple.main:([Ljava/lang/String;)V bytecode-index 15: FAILURE
[java::my.petty.examples.Simple.main:([Ljava/lang/String;)V.null-pointer-exception.4] Throw null: SUCCESS
[java::my.petty.examples.Simple.<clinit>:()V.null-pointer-exception.1] Throw null: SUCCESS
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS


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

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

JBMC provides you many command line options allowing you to customize its analysis. The options are listed here. You can also obtain their listing by using the option --help.

 

JBMC Download

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.