~~NOTOC~~

====== 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.