Compiler Design Lab

Jobs

Student Projects

At the Compiler Design Lab, we can offer a range of bachelor and master thesis topics. For some inspiration, a selection of proposed topics can be found below.

These are mostly ideas for possible topics. Do not hesitate to contact Sebastian Hack if you are interested in a thesis / hiwi job in the compiler space. We then can discuss topics suiting your interests.

Formal Verification of the Preservation of Security Properties through Compiler Passes

Compiler passes or optimisations often don't preserve important security properties which are widely used to prevent side-channel attacks.
There are many open questions about which optimisations do preserve which security properties.
Hyper-simulations (a hyper-simulation is basically a two-dimensional simulation) provide the means to formally verify the preservation of security properties.
Security properties to be examined include the constant-time property, non-interference, equal execution time (with some dedicated timing model) and non-malleable information flow.
In particular, it would be interesting to show the preservation of non-interference through a linearisation, spilling and register allocation pass.
Another option would be to prove the preservation of equal execution time or non-malleable information flow through some compiler passes.

Your own ideas within this general topic are also very welcome.
To do the formal proofs the student should have a solid Coq background (e.g. by having passed ICL).

Contact: Julian Rosemann.

Evaluation of SK Calculus as a Compiler Backend

This thesis aims to investigate the potential use of the SK calculus as a backend for compilers. The study will focus on analyzing the performance overhead of SK calculus's simplistic representation, determining the minimum set of instructions and environment required for optimal performance, comparing integer encoding versus native encoding trade-offs, and evaluating the advantages of using the SK calculus as a compiler backend.

Research questions:

  1. What is the performance overhead of the SK calculus's simplistic representation when used as a compiler backend?
  2. What is the minimum set of instructions and environment required for optimal performance when using the SK calculus as a compiler backend?
  3. How does integer encoding compare with native encoding when using the SK calculus as a compiler backend?
  4. How do optimizations relate and influence the representation?
  5. What are the advantages of using the SK calculus as a compiler backend?

Related concepts: BF, GRIN, Miranda, Bootstrapping, RISC vs CISC

Contact: Marcel Ullrich

Compiler Optimizations in Slicing for 3D Printers

3D Printers are an emerging field used in experimental research by physicists and engineers. The software stack for 3D printers mainly focuses on usability and user experience. Simultanously, machine learning algorithms have shown to be useful in optimizing the resulting g-code (movement instructions) produced by the slicer. In this project, we aim to study traditional compiler and optimizations techniques to produce optimized g-code for 3D printers.

Research questions:

  1. Should there be an intermediate representation (IR) between the STL (model) and GCode (movement) layer?
  2. How can compiler optimizations be applied to model construction and slicing?
  3. Can one slicer generate code for different printer axis-systems?

Related concepts: Synthesis, Constraint Programming, Machine Learning, Electronics

Contact: Marcel Ullrich

Integrating the Region Vectorizer

The Region Vectorizer is a vectorization framework for LLVM developed at the Compiler Design Lab. RV has been very successful in vectorizing SIMT code with complex control flow and is the most versatile framework for LLVM in that area out there. Yet, wider popularity and adoption of RV has been held back by the lack of integration with a major programming language compiler. Your thesis in this topic would deal with the integration of RV in a popular LLVM-based compiler. This may include working the community surrounding that language. A successful integration would be highly visible in the LLVM and language communities.
Candidate languages:

Contact: Joachim Meyer