Java PathFinder

A Formal Methods Tool for Java


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 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