Developer Guide

From the previous sections, you know that JPF is a collection of interchangeable components. In this guide:

Core Mechanisms

• ChoiceGenerators – Non-deterministic choice handling
• Partial Order Reduction – State-space optimization
• Slot and Field Attributes – Custom data storage

Extension Mechanisms

• Listeners – Event-driven JPF extensions
• Search Strategies – Custom exploration algorithms
• Model Java Interface (MJI) – Native method modeling
• Bytecode Factories – Custom instruction implementations

Utilities

• Logging System – JPF’s logging infrastructure
• Reporting System – Output and result reporting
• Running JPF from Application – Embedding JPF

Development Process

• Coding Conventions – JPF coding standards
• Creating Projects – New JPF project setup
• Modules – JPF module architecture