Thesis Topics in Software Science

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. There are many different kinds of topic that can contribute to such an ambitious project:

  • Development. Good student projects involve replicating and/or comparing existing analyses, such as heap analysis based on separation logic, within our framework. For this kind of thesis, you need some experience with functional programming. For inspiration, you may have a look at our open issues tracked on the Goblint Github page.
  • Benchmarking. We would greatly appreciate help on developing the infrastructure around Goblint; in particular, the testing and benchmarking of the analyzer are based on old ruby scripts. Over the years, people have added new scripts for each new scenario. The good news is that we now know all the requirements, so it's time to build GobExec, a unified framework in Python that supports all our benchmarking needs.
  • Analysis. For a genuinely high-impact thesis, you may try to use Goblint on the Linux kernel or OpenSSL. Consider a version where a known vulnerability has been found and help us get goblint to identify the vulnerability without emitting too many false positives. This requires understanding C and an interest to really understand Linux kernel code.
  • Usability. We have recently been working on interactive analysis and trying to make our analyzer usable for the wider public to verify programs. There are some simpler topics available here, such as extending our user interface, GobPie, to allow the configuration of our analyzer.

Contact: 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.

Other Stuff

We can supervise other topics related to programming languages and verification.

  • Kalmer Apinis has a list of topics.
  • Vesal Vojdani can offer topics to improve our compiler construction course.
  • You can offer your own topic if you are highly motivated and need minimal guidance. :)