Below you find a very brief overview of the projects that students did the last four years.

The goal is to improve the listener gov.nasa.jpf.listener.MethodTracker.

The goal is to improve the listener gov.nasa.jpf.listener.NoStateCycles.

The goal is to update the JPF plugin for Eclipse so that it works with version 4.10.

The goal is to develop a listener that tracks variables.

The goal is to develop a listener that stores the state space as an adjacency matrix and an adjacency list.

The goal is to improve the listener gov.nasa.jpf.listener.StackDepthChecker.

The goal is to document some of JPF's search listeners.

The goal is to improve the listener gov.nasa.jpf.listener.NumericValueChecker.

The goal is to improve the listener gov.nasa.jpf.listener.VarTracker.

The goal is to develop an extension of JPF that tracks aliasing in Java.

The goal is to develop an extension of JPF that allows the user to view and analyze the state space of the system under test in a 3D environment.

The goal is to make the beam search algorithm, developed in one of the labs, customizable.

The goal is to enhance the JPF listener called EndlessLoopDetector.

The goal is to extend jpf-jmt (see below) with

• state space graph listener which prints graph with memory usage at each state
• constraint that allows limiting memory usage of application

The purpose of this project is to develop a listener to warn when round off errors could possibly occur by a number of different mathematical operations and situations.

The goal is to implement a listener that will track the lifecycle states of an object within a given program.

The goal of this project is to explore JPF's reporting system by extending the publisher to handle different formats such as JSON and HTML.

The goal of this project is to use JPF to capture input, in particular input obtained from the keyboard or a graphical user interface.

The goal of this project is to use JPF to inspect the values of local variables at break points.

The goal of this extension of JPF, named jpf-jmt, is to provide accurate reporting of memory usage.

This project will be based on an android puzzle game with levels composed mainly of two objects: a ring and a circle. The project goal is to use JPF to determine the shortest path to reach a level complete state and create random levels.

The goal of this project is to use JPF to check whether a concurrent data structure is linearizable.

The goal of this project is to extend JPF so that it can check Java applications that use the JDBC API.

The goal of this JPF project is to implement a listener that tracks and logs all variables that are affected by a random variable.