This year’s annual Java PathFinder (JPF) workshop was held May 1– 2, 2008 at the Fujitsu Laboratories campus in Sunnyvale, CA. It was attended by participants from industry, government organizations, and academia, who came from as far as the University of Durham, UK, and the University of Tokyo, Japan. The two days were packed with talks spanning a gamut from JPF tutorials to presentations of ongoing JPF applications.
This year’s focus was on two topics: JPF usage within Fujitsu’s WEAVE project for model checking web applications, and presenting the new, bytecode-based symbolic execution mode of JPF. The workshop also featured sessions about optimization topics and JPF’s participation in Google’s Summer of Code.
The workshop was widely regarded as a success, demonstrating that—in its third year of open sourcing—JPF has gained a strong user community among both researchers and application developers.
BACKGROUND: JPF is a tool suite for software model checking of Java bytecode programs. It is used as a replacement of the “java” command, to execute applications in a variety of ways in order to find program defects like deadlocks and unhandled exceptions. JPF can systematically explore different thread scheduling sequences, and supports variation of test data with user-defined heuristics. There are various extensions for guided model checking, symbolic execution, compositional verification, and numerical analysis.
NASA PROGRAM FUNDING: Exploration Systems Mission Directorate, Exploration Technology Development Program
Contact: Peter Mehlitz