PV3 Java Pathfinder (aka jpf-core, aka JPF)checks properties of annotated Java code

Application domain/field

Type of tool

Model checker

Expected input


Expected output

The system can report on 3 different things:
  1. System under test (SUT) output: what is the SUT doing?
  2. JPF logging: what is JPF doing?
  3. JPF reporting system: result of the JPF run
The last option is probably the most interesting for users. This will report any property violations. Per property violation it can show the type of error, a trace leading to the violation, give a snapshot of all threads when the violation occurs, show the program output for the trace and some statistics.


Software model checker for Java bytecode programs


It is possible to run Java Pathfinder from within NetBeans or Eclipse (with and without a plugin) as well as from a Java program or the command line.
Java Model checking


Related papers

Java Pathfinder at SV-COMP 2019 (Competition Contribution)

Last publication date

4 April 2019

Related tools

The wiki contains a list of tools that use JPF: https://github.com/javapathfinder/jpf-core/wiki/Projects

ProVerB specific

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