The control flow of first-order (recursive) procedural programs can be accurately modelled by pushdown automata. Moped is a leading (symbolic) implementation of just such a modeller; it has been the back-end engine of choice of a number of influential software model checkers. The current version of Moped uses symbolic representation techniques, and has an input language that resembles a simple imperative programming language called Remopla.

Jimple is an intermediate representation of a Java program and language for it, designed as an alternative to the stack-based bytecode. It is typed and a form of conventional three-address code (thus making it suitable for optimzation). An attractive feature of Jimple (as an intermediate language for program analysis) is that it consists of only 15 different possible operations (by comparison, Java bytecode supports more than 200 different operations).

The aim of the project is to construct a compiler from Jimple to Moped. The compiler will serve as the back-end engine of a reachability / LTL model checker for Java.

This is a partner project of "A model checker for Java".

Relevant courses