Looking at the JPF directory structure, you notice a whole extensions tree, which in turn contains sub-directories that resemble the JPF toplevel structure. These so called JPF Extension Projects represent JPF adaptations for specific application types, property classes, or output artifacts (like test cases). The most prominent example is the symbolic execution mode to generate concrete tests.
While there is no strict rule for what constitutes a JPF extension (other than core classes not being allowed to depend on them), a common feature is that they replace or add classes in/to the JPF core packages, like different instruction set implementations, different MJI libraries, or even replaced VMs. Theoretically these extensions could just replace core classes, but it usually is much better to keep them in separate packages and use one of the various configurable JPF interfaces (like the BytecodeFactory) to bring them in. This ensures that JPF can be built in IDE's like Eclipse without the need to modify classpaths.
It should be noted though that extension projects are not built or tested automatically when using the Ant build system. If this is required, a build.xml has to be provided for the extension, which can be processed by using some generic macros in the JPF Ant system. Please refer to the Building JPF from the Command Line documentation for details.
Because there is no dependency of core classes or other JPF parts on a JPF extension, this is also a good "sandbox" to try out and share new functionality of common interest, the side effect of this being that extenions should be considered less stable than the rest of the system.
Currently, the major JPF extensions are:
ui -
User Interface Model Checking
This is an example of model checking a specific class of Java applications -
Swing and AWT programs. The extension is implemented as a set of MJI modeled
standard libraries that replace javax.swing.* and java.awt.* functionality so that
standard Java user interface applications can be tested for various different
user inputs.
symbc - Symbolic Test Data Generation The symbolic execution extension uses a BytecodeFactory to override JPF's core bytecodes to generate concrete test cases. In a nutshell, this works by using the JPF field/stackframe attribute system to collect symbolic path conditions, which are then fed into a contraint solver to obtain concrete test data. The choice points in this execution mode are branch instructions.
symts - Symbolic Threadsafety Test Generation This is a very simple "symbolic" execution mode that tries to identify potential thread safety problems, and then creates code to test this with concrete value JPF execution mode. The symbolic information is much more simple than with the symbc extension, and can be kept in the execution trace. The first implemented test category detects un-synchronized access of fields from within the same public (exported) method, to identify candidates for the PreciseRaceDetector listener.
cv - Compositional Verification Framework The CV extension implements a machine learning algorithm that can be used for assume/guarantee reasoning, to partition a system into components that can be verified separately. Ultimately, the goal of this extension is to dramatically improve the scalability of JPF, but it can be also used to generate environment assumptions for the UML model checking, to determine "valid" event sequences. This extension is mostly implemented with JPF listeners.
numeric - Numeric Property Verification This bytecode replacement extension started as a set of numeric instruction classes to detect over/underflow, but got extended to also include inexact value propagation (NaN, Inf), exact floating point comparison, and potential catastrophic cancellation (loss of precision by subtraction/addition)
statechart - UML State Chart Model Checking The state chart framework is a variation of the user interface model checking, for the purpose of model checking UML state chart diagrams. It is a combination of MJI libraries that are based on a unique translation scheme for UML state charts, together with generic applications (test drivers) to execute these state charts. The framework supports both testing and model checking, using the same scripting language for environment specification.