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).
Notes:
- In principle this project is automation-focused, but there is a research component: finding the right way to automate the methods is a challenging project in the area of automated reasoning. On top of that, sometimes the proofs for the existing methods need to be updated for a slightly different formalism.
- Depending on your preferences, there is also a more theory-focused possibility to define your own new methods, or improvements to existing methods.
- For Bachelor students, this is about first-order term rewriting systems, much like the ones discussed in the semantics and rewriting course. Master students may also choose to work on higher-order term rewriting systems instead.
- There are annual competitions for tools that analyse termination, complexity or confluence of term rewriting systems. If you are ambitious, we can aim to have your tool participate in these competitions, and perhaps even publish a tool paper in a conference or workshpo.
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.
Notes:
- This could either focus on the theory side (formally proving the transformation correct using program semantics), on the implementation side (defining a translation from a large language fragment and fully implementing it), the optimisation side (defining a basic translation and then finding ways to make the resulting system more manageable, for example by combining rules or applying methods like separation logic).
- Understanding of how to use parser generators such as ANTLR (or how to write your own parser) is very beneficial for this project, especially if you focus on the implementation side.
- This does not need to be limited to imperative languages: translations from for instance OCaml or Haskell, or translations from java that include the object-oriented features, would offer a larger research / program semantics component.
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:
- Invariant generation for termination: like finding loop invariants for C code, you would find ways to automatically derive properties that are preserved during recursion. This project would involve literature research on invariant generation, mathematical reasoning to see which methods apply.
- Adapting termination methods (Master project): take an existing method to prove termination or non-termination of term rewriting systems, and show how it can be adapted to systems with constraints.
- Constraint simplification on array programs: write a kind of SMT solver for the theory of integer arrays, which also has the possibility to simplify constraints.
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.