Open Theses

Goblint

Goblint is a static analyzer written in OCaml for the analysis of multi-threaded C programs. Goblint is developed jointly at our chair and the Chair of Programming Languages and Systems at the University of Tartu. Students interested in bachelor and master theses on Goblint should usually have gained experience in functional programming as well as on abstract interpretation, e.g. by having completed the program optimization course. For inspiration, you may have a look at our open issues tracked on the Goblint Github page. If you want to do a student thesis related to Goblint, you may contact Ali Kocal or Michael Petter.

Two examples of Currently Open Topics:

• BA: Analyzing Next-Generation C code with Goblint. 
  Goblint should be extended to support features of C11, so we can analyze programs using C11 features. This will provide you with insights into the C standard, Compiler Construction, and Static Analysis by Abstract Interpretation.
  A succesful applicant should have attended either the Compiler Construction or the Program Optimization lecture.
• BA: Counterexamples for SV-COMP.
  To complement Goblint's ability to prove programs safe, we have recently implemented an underapproximative technique to generate counter examples based on Local Traces. The goal of this thesis is to extract counterexamples in the format required for the Software Verification Competition, and to enhance the prototype implementation (w.r.t. performance and coverage of the C standard) in order to allow Goblint to also create counterexamples in next year's competition.
  A successful applicant should have programming skills in OCaml and be interested in learning about static analysis, having taken Program Optimization is not a requirement in this case.

These are (likely) not the only open topic that we can offer about Goblint. If you are interested in this topic or want to hear about other topics, contact us.

Formalization of Fixpoint Solvers in Isabelle/HOL

Fixpoint solvers are at the core of static analyzers. Their correctness is crucial for static analyzers to produce reliable results. We are working on formalizing the top-down solver and different variants of it in Isabelle/HOL. Feel free to contact Sarah Tilscher or Alexandra Graß if you are interested in a thesis topic related to this area. Most topics require some experience with Isabelle, interactive theorem proving or functional programming.

Currently open topics could be:

• BA: Refining Code-Generation for Top-Down Solvers in Isabelle
• MA: Verification of a Top-Down Solver with Side-Effects in Isabelle

Compiler Construction

In this block we want to enrich the Flipped Classroom concept of Compiler Construction with web-based interactive trainings, just like these. These topics require to have attended Compiler Construction IN2227 beforehand. If you want to do a thesis in this area, contact Michael Petter.

• BA: Refining the Tutors for Typechecking and Structural Subtyping
  In this module, we want to add more interactivity to the existing webtutor for typechecking and subtyping.

Optimization Algorithms, Tools, and Frameworks for Quantum Computing

Currently MQV (Munich Quantum Valley)  is building a quantum computer and promoting quantum science and quantum technologies in Bavaria. We, as researchers in MQV, are working with many research groups to build a quantum computing ecosystem.  For that we face challenges in areas like quantum programming language (E.g., design, compilation, and optimization of programming languages that deal with quantum specific features and/or classical control signal), quantum algorithms (E.g., mapping and routing algorithms that equip circuits with hardware-specific properties), tools/frameworks (could be one that helps perform analysis for quantum specific problems, one that helps users to design quantum circuits, or one that provides interfaces amongst different functional modules in quantum computing). Feel free to contact Yanbin Chen if you wish to discuss further, so that we could develop some thesis topic that is tailored to both your personal interests and our ongoing research.

Other topics

If you are interested in working on other topics related to compiler construction or static analysis, you may contact any member of the chair via e-mail.

Completed Theses ✓

This is an incomplete list of some of the theses that were completed at our chair since the middle of 2019.

Bachelor's thesis

Webtutor for Testing Strong Acyclicity of Attribute Systems (Alexey Glushik, BA 06/22)
Webtutor for Structural Subtyping and Type Checking (Dávid Endrédi, BA 05/22)
Webtutor the Berry Sethi Construction (Valentin Bertle, BA 05/22)
Towards an integration of Sarif into Goblint (Alexander Eichler, BA 10/21)
A Continuous Integration and Testing Platform for the Static Analyzer Goblint (Andreas Ferrano, BA 04/21)
Adding Support for C99 and C11 to the Goblint Static Analyzer (Coşku Barış Coşlu, BA 10/20)
Extending a Syntactic Search in C Source Code with Analysis Results from the Static Analyzer Goblint (Elias Brandstetter, BA 09/20)
Comparison of Analyses in CIL and Goblint (Kerem Cakirer, BA 09/20)
Syntactical Search in C Source Code (Olga Faddeenkov, BA 07/20)
User Interface for Program Analyzer Goblint using a OCaml-JavaScript Transpiler (Alex Micheli, BA 05/20)
LR Parser Tutor (Leo Fahrbach, BA 20)

Master's thesis

Combining Analyses of Different Precision in the Goblint Static Analyzer (Florian Stamer, MA 11/21)
Improved Abstract Domains for Structs in the Static Analyzer Goblint (Jakob Erzar, MA 10/21)
Refining Incremental Abstract Interpretation in Goblint (Sarah Tilscher, MA 07/21)
Liveness Analysis of Multi-Threaded C with Posix Threads (Denis Grebennicov, MA 05/21)
Implementation and Comparison of Precision of Various Abstract Domains in the Program Analyzer Goblint (Dymtro Yakymets, MA 11/20)
Incremental Static Analysis with Goblint (Julian Erhard, MA 04/19)
Sound Yet Precise Modelling of Arrays in Abstract Interpretation (Michael Schwarz, MA 04/19)