PV3 JBMCchecks user-defined assertions and runtime exceptions in Java code

Application domain/field

Type of tool

Model checker

Expected input


Expected output

Whether the verification failed or succeeded. It will show a list of defects and whether they were verified ('SUCCESS') or not ('FAILURE').


Bounded model checker for Java bytecode. It checks runtime exceptions (e.g. nullpointer exceptions) and user-defined assertions Uses SAT/SMT solver (no specific one mentioned). Built on top of CProver. Tool paper calls it an extension to CBMC. It is possible to configure JBMC by passing arguments when calling JBMC. For example one can choose to disable certain checks (e.g. division by zero checks). For more information on the configurations, see: https://www.cprover.org/jbmc/command_line_options.html
Java Model checking


Related papers

Last publication date

4 April 2019

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.