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

Application domain/field

• Model checking
• Software model checking
• Bytecode

Type of tool

Model checker

Expected input

• Java program (possibly with annotations)
• Optionally: configuration files

Format:

• .class or .java (Java program)
• .jpf file, jpf.properties file, .jpf/site.properties file (for application properties, project properties and site properties respectively)

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.

Internals

Software model checker for Java bytecode programs

Comments

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.