Java PathFinder
A Formal Methods Tool for Java
Abstract
The Java PathFinder, JPF, is a
translator from a subset of Java 1.0 to PROMELA, the programming language of
the
SPIN
model checker. The purpose of JPF is
to establish a framework for verification and debugging of Java programs
based on model checking. The system is especially suited for analyzing
multi-threaded Java applications, where normal testing usually falls short.
The system can find deadlocks and violations of boolean assertions stated by
the programmer in a special assertion language. The user guide explains in
detail how to use the system. Please contact Klaus Havelund
Klaus.Havelund@jpl.nasa.gov
for details about installation.
User Guide
Java PathFinder User Guide (K. Havelund)
[ps,
ps.Z
]
(Tech. Report)
Published Papers
Model Checking Java Programs Using Java PathFinder
(K. Havelund, T. Pressburger)
[ps,
ps.Z
]
(International Journal on Software Tools for Technology Transfer, STTT,
2(4) April 2000. Special issue containing selected submissions for the
4'th SPIN workshop, Paris, November, 1998)
Applying Model Checking in Java Verification
(K. Havelund, J. Skakkebaek)
[ps,
ps.Z
]
(6th SPIN Workshop in connection with FM99 Toulouse)
Named after
Mars PathFinder
Created by Klaus Havelund
Last modified: April 23, 2000