Java PathFinder
The Java PathFinder, JPF, is a translator from Java to Promela,
the programming language of the SPIN model checker. The purpose is
to establish a framework for verification and debugging of Java programs
using model checking. The system detects deadlocks and violations of
assertions stated by the programmer.
- Developer:Klaus Havelund
- Contact:
-
Klaus Havelund
NASA Ames Research Center
Moffett Field, CA 94035-1000 USA
Building 269, 2 floor
(Silicon Valley area)
phone : (+1)650-604-3366
email : havelund@ptolemy.arc.nasa.gov
- Number of sites:1
- Number of users:6
- In use: since 1999
- Language: Moscow ML and Common LISP
- Compilers: Moscow ML and Franz Allegro LISP
- Line count: about 5K
- Availability:Available for internal use and on request for beta test.
Please send an email if interested.
- Related publications:
-
"Model Checking Java Programs Using Java PathFinder"
Klaus Havelund and Thomas Pressburger
To appear in the journal : "Software Tools for Technology Transfer" (STTT)
-
"Practical Application of Model Checking in Software Verification"
Klaus Havelund and Jens Skakkebaek
Submitted for publication.