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.

Exploring Program Equivalence Techniques: From Invariance Mining to Fuzzing

This thesis will investigate approximate program equivalence techniques, including invariance mining, automatic verification, functional equivalence using fuzzing and runtime checks, and language-independent program equivalence. The goal is to compare and contrast these techniques, identify their strengths and limitations, and evaluate their effectiveness in detecting program equivalence. An additional focus lies on identifying a minimal knowledge base to establish functional equivalence.

Research Questions:

  1. What are the different techniques for program equivalence, and how do they differ from one another?
  2. How effective are these techniques in detecting program equivalence, and what are their limitations?
  3. How can these techniques be combined to improve their effectiveness?
  4. How can program equivalence tools be adapted for different programming languages and platforms? Can equivalence be established independent of concrete languages?

Related: Fuzzing, Synthesis, Separation Logic, Automated Reasoning, Verification, Model Checking

Contact: Marcel Ullrich

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 for Factorio: A DSL Approach to Factory Optimization

This research idea proposes to use compiler optimization techniques to improve the performance of Factorio factories by developing a domain-specific language (DSL) for designing and optimizing factory layouts. The study will compare the efficiency of different circuit layouting techniques, including FPGA synthesis and circuit languages such as Verilog, and explore the relationship between compiler optimizations and factory optimizations.

Research questions:

  1. What compiler optimization techniques can be applied to improve the performance of Factorio factories?
  2. How can a DSL be developed to facilitate the design and optimization of Factorio factory layouts?
  3. What are the comparative advantages and limitations of different circuit layouting techniques in the context of Factorio factory optimization?
  4. How can compiler optimizations be related to factory optimizations, and what insights can be gained from this relationship?

Related: Synthesis, Circuit design, Cross-language communication, modding, optimization (scheduling, layout, code optimization), DSL

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