Java Pathfinder

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. == Limitations ==

• JPF cannot analyze Java native methods. If the system under test calls such methods, these have to be provided within peer classes, or intercepted by listeners • as a model checker, JPF is susceptible to Combinatorial explosion, although it performs on-the-fly Partial order reduction • the configuration system for JPF modules and runtime options can be complex == See also ==