Thesis Topics in Software Science

We can supervise topics related to programming languages and verification:

  • Vesal Vojdani: Software science, Compiler construction course.
  • Danel Ahman: Algebraic effects, Asynchrony, Temporal resources, F*, Agda, Logic in Computer Science course.
  • Kalmer Apinis: Functional programming, Program Analysis, Coq.
  • Simmo Saan: Goblint, Compiler construction course.
  • Bruno Rucy: Query Optimisation, Ontologies, Logic Programming.
  • You can offer your own topic if you are highly motivated and need minimal guidance. :)

We are interested in techniques that provide strong guarantees that software systems work as intended. Our expertise is in the field of sound static analysis using abstract interpretation. We can best share our (vast ocean of) knowledge if you choose a topic related to 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.

DeepMOOC: Program analysis for teaching

We have started a project to apply program analysis techniques to improve the quality of machine feedback provided in our programming courses. There are many conceivable topics here, but one concrete analysis would be the static estimation of time complexity. Also, much work is needed to integrate existing checkers into a coherent platform that provides semi-automated feedback to students.

Contact: Ahti Põder.