Java Pathfinder (JPF) Core System

The JPF Core System is a framework to analyze and verify Java bytecode programs. The major component of JPF core is an extensible and runtime-configurable virtual machine (VM) that can be customized with runtime components such as specific instruction sets and plug-ins to observe program execution. The JPF core can store and restore program states, and comes with a configuration that constitutes a standalone software model checker that can be used to detect and analyze concurrency defects in Java applications like deadlocks or data race conditions.