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. You may browse student-job label on Github, but we recommend the following this year:
- Code Coverage Reports for Static Analysis. In software testing, code coverage is used to measure and visualize which parts of the program are executed by a test suite to discover untested code. The goal of this thesis is to produce similar reports from static analysis to discover unanalyzed code. It requires simple OCaml programming and little knowledge of Goblint's analyses.
Coloring Data Race Interference Graphs.Goblint detects and reports data races based on an interference graph of memory accesses. The goal of this thesis is to apply graph coloring algorithms to such graphs and improve Goblint's race warnings using this information. It requires OCaml programming and understanding of Goblint's race analysis.
- GobExec for testing. For over 16 years, Goblint has been tested using a Ruby script which no longer fulfills our testing needs. The goal of this thesis is to extend GobExec, a new benchmarking framework for Goblint, with testing support to replace our existing script. It requires advanced Python programming and minimal knowledge of Goblint itself.
Contact: Simmo Saan.
Applied Automated Software Verification
There are many highly sophisticated automated software verifiers, such as those competing at the International Contest on Software Verification, but applying these advanced methods on real-world programs to obtain high signal has proven challenging. To make the software more safe and secure would be how to apply these tools in the real world. I have a couple of ideas in this direction:
- CoOpeRace: Cooperative Race Detection as a Service. This is a grand idea inspired by the CoVeriTeam Service with a focus on the specifics of comparing race detection results. [One student working on the framework side of this, but topics are possible on how to achieve true cooperation between the tools.]
- Evaluating Sound Static Analyzers. It's not so clear what various static analyzers can do. The SAMATE project at NIST aims to evaluate and showcase tools. It would be great to create a simpler and more user-friendly introduction to their work. Try running goblint on their suite, and possibly, generalize the method so that any automated verifier at SV-COMP could run on the SAMATE Ockham evaluation criteria for sound analyzers.
- Case Studies on Real-World Security Vulnerability Detection. 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.
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.
We can supervise other topics related to programming languages and verification.