A quick roadmap of the next two days, followed by a 10,000mi overview of what happened during the last year, what is going on right now, and what will drive JPF's development in the forseeable future.

It's been 3 years now since JPF has been open sourced, so we will reflect a bit on what has been achieved, and what has yet to come. There always has been a struggle about what programs to check with JPF - models or Java production code. The jury stayed out for so long that it finally became obsolete: we do both. We will talk about this both on the basis of JPF's design, and a classification of JPF application types that are:

• JPF unaware
• JPF enabled
• JPF dependent

For each of these categories, we will highlight the strengths and needs of JPF.

• PDF slides

In this talk, we will cover major infrastructure developments and examples for all three of the aforementioned application types, namely:

• the UML statechart model checking framework (JPF extensions / dependent apps)
• the generic Attribute System (JPF core / independent apps)
• Bytecode Factories to change execution semantics (JPF core / independent apps)
• the extensible Reporting System to produce structured output (JPF core)
• using Java annotations for JPF test specs and programming-by-contract support (JPF aware apps)

There are two intentions for this talk: (1) present new extension mechanisms and potential examples, (2) confuse the audience with a wild hodgepodge of topics. In fact, (2) is what puts the classification of the first talk to test, so that we never get lost in the realm of JPF (and the following talks).

• PDF slides

Google's Summer of Code program provides funding for students to spend their summer working on open-source software. This year, Java PathFinder applied and was one of 175 projects accepted into the program. I'll provide an overview of the goals of GSoC and how it works. Then I'll briefly present the students we selected and the projects they will be working on this summer.

Java PathFinder (JPF) was used to generate object graphs as test inputs for object-oriented programs. Specifically, JPF was used as an implementation engine for the Korat algorithm. Korat takes two inputsÑa Java predicate that encodes properties of desired object graphs and a bound on the size of the graphÑand generates all graphs (within the given bound) that satisfy the encoded properties.

This talk presents our results on speeding up Korat search in JPF. The experiments on ten data structure subjects show that our modifications of JPF reduce the search time by over an order of magnitude.

Joint work with Milos Gligoric, Tihomir Gvero, Steven Lauterburg, and Darko Marinov

• PDF slides

Java PathFinder (JPF) is an explicit-state model checker for Java programs. JPF implements a backtrackable Java Virtual Machine (JVM) that provides non-deterministic choices and control over thread scheduling. JPF is itself implemented in Java and runs on top of a host JVM. JPF represents the JVM state of the program being checked and performs three main operations on this state representation: bytecode execution, state backtracking, and state comparison.

This talk summarizes four extensions that we have developed to the JPF state representation and operations. One extension provides a new functionality to JPF, and three extensions improve performance of JPF in various scenarios. Some of our code has already been included in publicly available JPF.

Joint work with Tihomir Gvero, Milos Gligoric, Steven Lauterburg, Marcelo d'Amorim, and Sarfraz Khurshid

• PDF slides

As multi-agent systems become more and more widely used, a vast array of different agent programming languages have emerged. The use in increasingly complex and critical areas leads to a need to analyse comprehensively the behaviour of such systems. The Agent Infrastructure Layer (AIL) is a Java toolkit that allows multi-agent programs written in many BDI languages to be verified in a uniform framework. For verification we use a customised version of JPF. Agent JPF (AJPF) uses a property specification languages based on LTL and enriched by agent-specific modalities.

• PDF slides

We present a framework for easy and precise capture of temporal logic requirements in Web Applications using a novel template-based specification language. The framework includes automatic monitor generation from the requirement specification as well as a middleware to automatically model check strong heap properties by interfacing this monitor to the JPF JVM heap

Formal verification techniques usually work for closed homogeneous non-distributed applications. For example, Java model checkers such as JPF work for Java programs that are ready to run on a single JVM. However, web applications are usually comprised of artifacts written in many languages (e.g., Java, JavaScript, HTML, XML). They are to be deployed in a distributed environment and to interact with users through a web browser. To apply JPF to web applications, all non-Java components need to be represented in Java. In addition, the distributed nature of a web application needs to be dealt with so that the resulting Java program is non-distributed but preserves relevant, to the properties being checked, behaviors of the original application. In this work, we present environment generation for web applications, which transforms open heterogeneous distributed web applications, mainly written in Java, into closed homogeneous non-distributed Java programs, ready to be analyzed by JPF.

Whole program analysis through symbolic execution can be powerful but computationally intensive. In this paper we present a technique whereby static analysis is used to help in efficiently transforming a Java program for symbolic execution. First, a context-sensitive relevancy analysis algorithm is utilized to pin-point locations in the program where symbolic values can flow into. This information is utilized by a code instrumenter that transforms only the relevant parts of the Java program with symbolic constructs. When this transformed program is run through a state-based model checker that explores possible program paths, all possible data values on symbolic variables are examined through a decision procedure solver or through an FSM library in case of symbolic strings. Program requirements are checked through assertions in the program. Experiments demonstrate that this technique can greatly improve the performance of the symbolic execution engine over a simple technique that blindly instruments the whole program.

We describe an approach to testing complex safety critical software that combines unit-level symbolic execution and system-level concrete execution for generating test cases that satisfy user-specified testing criteria. We have developed a symbolic execution framework that implements a non-standard bytecode interpreter on top of the Java PathFinder model checking tool. The framework propagates the symbolic information via attributes associated with the program data. Furthermore, we describe two techniques that use system-level concrete program executions to gather information about a unit's input to improve the precision of the unit-level test case generation. We applied our approach to testing a prototype NASA flight software component. Our analysis helped discover a serious bug that resulted in design changes to the software. Although we give our presentation in the context of a NASA project, we believe that our work is relevant for other critical systems that require thorough testing

• PDF slides
• Powerpoint slides

We present techniques and their tool implementation that target verification/debugging processes on C or C-like language (such as SpecC/SystemC language) descriptions for hardware systems. Both concrete value simulator (normal simulator) and symbolic simulator are integrated as a single tool so that test patterns that satisfy user-specific constraints can be efficiently generated. The implementation is based on an extended system dependence graph so that descriptions in various similar languages can also be processed. The constraints that users can specify include starting points, ending points, and intermediate points in the descriptions with conditions on variables. The goal is to come up with shorter simulation traces which illustrate possible bugs. The generated traces will be the starting points for bounded model checking tools, such as SPIN or JPF. Some preliminary experimental results are presented. We also discuss an extension of our method to JAVA programs. Since SpecC has notions of structural hierarchy, its associated techniques may be able to be applied to JAVA programs.

• Powerpoint slides

The MCP model checker allows C and C++ programs to be exhaustively analyzed for a variety of failure modes, particularly those related to concurrency. MCP is an explicit-state model checker that seeks to provide JPF-like capabilities with respect to C and C++ rather than Java.

We also present a technique based upon partial evaluation and constraint solving that makes it possible to automatically generate test cases for C++ code that are guaranteed to meet specified coverage criteria. An example is given based upon the Ares/Orion Onboard Abort Executive Flight Rule Checker.

This session will provide an introduction of how to use JPF. While JPF can be seen as a replacement for a normal JVM (i.e. a substitute for the java command), it has a huge number of options (that require some knowledge about JPF's basic design), and in fact comes with it's own, open configuration mechanism. To say the least, this can be confusing for new users. We will tame this beast by giving a quick overview of JPF's major components, followed by a number of standard examples, showing how to configure searches, properties, reports and more.

• PDF slides
• Powerpoint slides
• example sources