History and Credits

JPF has come a long way from it's beginnings in 1999. Five major phases stand out

  1. 1999 Java-to-Promela translator (using Spin as the model checker)
  2. 2000 JVM / standalone checker
  3. 2003 design and implementation of extension structure
  4. 2005 open sourcing of JPF
  5. 2006 JPF4 with unified ChoiceGenerators and new execution engine

During this time, many people and institutions have worked on and with JPF. The majority of work is still done by the Robust Software Engineering (RSE) group at the NASA Ames Research Center. The incomplete list of key contributors (in random order) includes:

Klaus Havelund, who had the original idea to create a software model checker based on Java.

Willem Visser is (together with Corina) the driving force behind the research part of JPF. He continues to drive it into exciting new places like symbolic model checking and test case generation.

Flavio Lerda did most of the work for phase 2, turning JPF from a translator into a VM

Corina Pasareanu continues to tweak JPF as a testbed for symbiosis of symbolic and explicit state model checking

John Penix fought through the NASA ranks to make the JPF open sourcing happen, not at least succeeding based on his reputation as one of the few people who actually have been able to find real defects with software model checking

Masoud Mansouri-Samani shielded the developers from configuration and distribution management in the dark ages of closed JPF sources

Owen O'Malley showed his programming skills by implementing the MD5 based state hashing (with an interesting red-black tree), a huge win in terms of state storage. Owen also added some java.io library support based on MJI.

Dimitra Giannakopoulou happily uses JPF to distribute her famous LTL2Buechi - automaton translator (e.g. used in the LTSA system), which is so good that it remains in the JPF distribution even while JPF's LTL search is currently defunct. The translator can be built and used independently from the rest of JPF.

Peter Mehlitz (the "refactorator") - trying to fill the Java holes, coming up with extension mechanisms, getting all this into a manageable package, and generally breaking things.

Peter Dillinger is a hacker (the good kind) who has made numerous random simplifications, optimizations, bug fixes, code clean-ups and migrations for JPF4. Currently building new, flexible infrastructure for matching visited states.