Extensibility
JPF is an open system that can be extended in a variety of ways. The main extension constructs are
- listeners - to implement complex properties (e.g. temporal properties)
- peer classes - to execute code at the host JVM level (instead of JPF), which is mostly used to implement native methods
- bytecode factories - to provide alternative execution semantics of bytecode instructions (e.g. to implement symbolic execution)
- choice generators - to implement state space branches such as scheduling choices or data value sets
- serializers - to implement program state abstractions
- publishers - to produce different output formats
- search policies - to use different program state space traversal algorithms
JPF includes a runtime module system to package such constructs into separate JPF extension projects. A number of such projects are available from the main JPF server, including a symbolic execution mode, numeric analysis, race condition detection for relaxed memory models, user interface model checking and many more.
Read more about this topic: Java Pathfinder