Bachelor and Master projects

For those interested in doing a Bachelor project, Master project, or research internship with me, I can particularly offer projects in the area of analysing term rewriting systems, or analysing programs by using term rewriting systems. Such projects can focus on the mathematical side (e.g., proving correctness of a methodology or developing a new one), on the semantics side (e.g., defining meaning-preserving translations from programming languages to rewriting), or on the tool develpoment side (e.g., implementing known verification methods by a clever use of SAT or SMT solvers).

Some example projects are listed below; ideas can be adapted to individual preferences. If any of these ideas appeal to you, or if you have a different project idea that you think may fall in my area of interest, please feel free to either send me an email, or drop by my office to discuss it (room 1.05a in the Mercator building).

Implementing TRS analysis techniques

There are many known techniques for termination, complexity and confluence analysis of term rewriting systems, but making a computer apply these automatically is no easy task. If you choose this kind of project, you will automate some of these existing methods, and implement them in the Java tool Cora (which already has functionality to represent all kinds of terms, and can handle the I/O).


Translating programs to constrained TRSs

You will define a translation from either a small toy language or a fragment of a real language like C or Java into constrained term rewriting systems. An example of this being done for a fragment of C is sketched in section 3 of this journal paper.


Analysing constrained term rewriting systems

Once a program has been translated to a constrained term rewriting system, we of course want to analyse it. However, the addition of logical constraints means that the existing techniques often do not apply directly. Instead, we could get to combine ideas from program verification with ideas from term rewriting analysis. Some example projects in this direction are:

All of the above projects would involve a literature study on existing methods (invariant generation, termination techniques or the inner workings of SMT solvers), mathematical reasoning to see which methods apply (or can be adapted to the new setting), and implementation using SAT and SMT solvers as backend.