What can be checked with JPF

Which defects can be found by JPF? Out of the box, JPF can search for deadlocks and unhandled exceptions (e.g. NullPointerExceptions and AssertionErrors), but the user can provide own property classes, or write listener-extensions to implement other property checks. A number of such extensions, like race condition and heap bounds checks are included in the JPF distribution

What programs can be checked by JPF? In general, JPF is capable of checking every Java program that does not depend on unsupported native methods. The JPF VM cannot execute platform specific, native code. This especially imposes a restriction on what standard libraries can be used from within the application under test. While it is possible to write these library versions (especially by using the Model Java Interface - MJI mechanism) there is currently no support for java.awt, java.net, and only limited support for java.io and Java's runtime reflection. Another restriction is given by JPF's state storage requirements, which effectively limits the size of checkable applications to ~10kloc (depending on their internal structure) if no application and property specific abstractions are used. Because of these library and size limitations, JPF so far has been mainly used for applications that are models, but require a full procedural programming language. JPF is especially useful to verify concurrent Java programs, due to its systematic exploration of scheduling sequences - an area which is particularly difficult for traditional testing.