Thesis Topics in Software Science

We supervise topics related to programming languages and verification. Ambitious students, especially those interested in potential Ph.D. positions, should first familiarize themselves with our Explainable Verification overview.

Click on the names of individual supervisors to see their proposed topics.

• Vesal Vojdani: Explainable verification, AKT and Software Security course material.
• Danel Ahman: Algebraic effects, Asynchrony, Temporal resources, F*, Agda, Logic in Computer Science course.
• Kalmer Apinis: Functional programming, Program Analysis, the Rocq Prover.
• Chad Nester: Category Theory, Programming Language Semantics, Logic
• Simmo Saan: Goblint, Compiler construction course.
• Bruno Carneiro: Query Optimisation, Ontologies, Logic Programming.

---

We develop and aim to maintain some useful experimental tools and languages. If you want to work on something more concrete, you may benefit from our (vast ocean of) knowledge while contributing to one of our pet projects:

Goblint: Race Detection World Champion

Goblint is a static analyzer written in OCaml for the analysis of multi-threaded C programs. Goblint is developed jointly with the Technical University of Munich. This is a very exciting and lively project, so we encourage our best students to use this opportunity to collaborate with the Crème de la Crème of European computer science.

Contacts: Simmo Saan, Vesal Vojdani.

Põder: Towards Explainable Static Analysis

Põder is a new sound analyzer for Java bytecode, written in Scala. It does not yet include all the sophisticated constraint solving algorithms that powered Goblint. We want to implement these algorithms and also prove their correctness. Here, you can either replicate most of Goblint’s functionality in Põder or proceed to certify these algorithms in Coq. It may be helpful to draw inspiration from the Iris framework where similar results are proven.

Contact: Kalmer Apinis.

Temporal Millet: Modal Types for Temporal Effects

Temporal Millet is a prototype programming language that combines modal types with graded effect systems to specify and verify temporal properties of program resources, with automatic checking via Hindley-Milner style type inference. It extends Matija Pretnar’s Millet with temporal algebraic effects and effect handlers whose operations are guaranteed to respect their declared time costs. A web UI is provided for demonstrating reductions.

Contact: Danel Ahman.