Model Checker for Java Programs
TBMG-2380
09/01/2007
- Content
Java Pathfinder (JPF) is a verification and testing environment for Java that integrates model checking, program analysis, and testing. JPF consists of a custom-made Java Virtual Machine (JVM) that interprets bytecode, combined with a search interface to allow the complete behavior of a Java program to be analyzed, including interleavings of concurrent programs. JPF is implemented in Java, and its architecture is highly modular to support rapid prototyping of new features.
- Citation
- "Model Checker for Java Programs," Mobility Engineering, September 1, 2007.