JPF has been both a research target and a system in use for a number of years. A broad collection of papers and reports is available, including the following (incomplete) list. Note that some of the older papers now have mostly historical relevance. JPF has undergone a lot of changes since 2000. If you need more recent information, esp. about the design and usage of current JPF versions, please consult the documentation.
“Model Checking Programs”. W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda. Automated Software Engineering Journal.Volume 10, Number 2, April 2003. link
“Addressing Dynamic Issues of Program Model Checking”. F. Lerda and W. Visser. Proccedings of SPIN2001. Toronto, May 2001. link
“Execution and Property Specifications for JPF-Android” Heila van der Merwe, Brink Van Der Merwe and Willem Visser. link
“JPF Verification of Habanero Java Programs” Peter Anderson, Brandon Chase and Eric Mercer.
“Formal Validation of Fault Management Design Solutions” Corrina Gibson, Robert Karban, Luigi Andolfato and John Day.
“Integrating JPF into Impendulo” (Extended Abstract) Pieter Jordaan, Willem Visser and Jaco Geldenhuys.
“A Knoppix-based demonstration environment for JPF” Richard Potter, Cyrille Valentin Artho, Kuniyasu Suzaki and Masami Hagiya.