Projects

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

Modifying MethodTracker

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

NoStateCycles Enhancement

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

JPF Plugin for Eclipse 4.10

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

Extending VMListener: Variable Tracking Functionality

The goal is to develop a listener that tracks variables.

Implementing AdjacencyMatrix and AdjacencyList Listener

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

JPF Update StackDepthChecker

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

Documenting Search Listeners

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

Improving Numerical Value Checker Listener

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

Improving VarTracker

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

Alias analysis

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

3D state space diagram

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.

A customizable beam search algorithm

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

Enhancing the EndlessLoopDetector listener

The goal is to enhance the JPF listener called EndlessLoopDetector.

Extension of jpf-jmt

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

Round off errors

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.

Object life cycle

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

Extending JPF's reporting system

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.

Capturing input

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

Break points

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

Java PathFinder Memory Tools

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

Circle Game Puzzle Solver & Generator

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.

Linearizability in JPF

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

JPF Database Modeling Code

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

Tracking Randomization in Java

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