Description

The FMT-based open source tool GROOVE can transform graphs (using user-provided rules describing the transformations) by adding and removing nodes and edges. Since the graphs can stand for pretty much any kind of system, ranging from computer networks to games, this is a very powerful and versatile modelling formalism.

One of the applications of graph transformation is to formally define operational semantics for programming and modelling languages. This principle has been demonstrated on some toy languages as well on a fragment of the programming language Java. This assignment is to extend the latter semantics to the entire language, up to and including the threading and locking mechanisms. If successful, the result will be the first full, formal semantic definition for Java.

This assignment requires a good understanding of the concepts of Compiler Construction (Vertalerbouw).

Additional Resources

1. The paper