This project aims to construct a reachability checker for a fragment of Java. Given a program of the fragment and a description of the test, the idea is to compile them to an appropriate Jimple representation using the Soot compiler. The reachability test is then performed by Moped, using a Jimple-to-Moped compiler (a partner project).

A task is to construct a graphical user-interface in the form of an Eclipse plug-in, to help user visualize progress of the verification process, and to enable user interaction with the analysis.

Time permitting, a number of extensions may be considered. For example, the checker can be extended to model-check LTL constraints, using a version of Moped that can verify LTL properties. A possible domain of application is inter-applet communications in multi-applet JavaCard code.

This is a partner project of "Compiling Jimple to Moped".

Relevant courses