(co-located with ASE 2011 )
November 12, 2011 Oread, Lawrence, Kansas
Java Pathfinder (JPF) is an automated open source analysis engine for Java programs. At the heart of JPF is an explicit state model checker. JPF is a customized Virtual Machine that enables the verification of Java bytecode. It checks for violation of properties and pre-defined software bugs such as null pointer exceptions, assertion violations, deadlocks, race-conditions etc. Key software model checking techniques such as state matching, partial order reduction, heap symmetry reduction, search strategies, heuristics, and listeners to monitor the execution of the programs are implemented within JPF.
JPF has well defined extension mechanisms, directory structures and build procedures that keeps the core stable and also makes the core easily extensible. JPF is engineered in a manner such that it provides a suitable and well separated sandbox for the implementation of new and alternative ideas in the domain of automated software verification and analysis techniques. As a consequence, the JPF toolkit consists of a large number of projects that are extensions of the core.
The submission site is now open. Submissions are through easy chair
We welcome contributions on all topics related to JPF or one of its extensions. In addition to research papers, we also solicit comparative analysis papers that evaluate algorithms in JPF or its extensions with relevant tools. The goal of the workshop is to encourage the flow of ideas relevant to JPF.
We solicit two kinds of papers:
Peter Mehlitz, NASA Ames
Neha Rungta, NASA Ames
Willem Visser, U. Stellenbosch