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

Application domain/field

• Model checking
• Bounded model checking
• Software model checking

Type of tool

Model checker

Expected input

• Compiled Java program (may include assertions)
• Number of times loops should be unwinded

Format:

• .class file (compiled Java program)
• integer passed as an argument when calling JBMC (number of loop unwinds)

Expected output

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

Internals

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