The Java Pathfinder Workshop 2011

(co-located with ASE 2011 )

Overview

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.

Submission Site

The submission site is now open. Submissions are through easy chair

Call for Contributions

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:

1. Full Papers: The full papers should be at most 12 pages long in the IEEE trans format. The paper should describe a fully matured research topic that has been implemented within JPF core or one of its extensions. The papers can be previously published at other peer-reviewed venues or be original research papers not been published before. In previously published work we highly encourage addition of new material that provides new insights about either the implementation, engineering, or evaluation with respect to JPF.
2. Short Papers: The short papers should be at most 5 pages long in the IEEE trans format. Short papers can describe an extension of JPF as a tool paper. Work in progress descriptions can also be submitted as short papers.

Important Dates

• Submission deadline: Aug 29, 2011
• Notification of acceptance/rejection: Sept 30, 2011
• Deadline for final version: Oct 15, 2011