Skip to content

Laboratory for Software Science

Thesis topics from Simmo Saan

This page lists concrete thesis topics I can offer (as of autumn 2026), but other related topics could be possible on request. You may be inspired by the list of defended theses which I (co-)supervised.

Goblint

My research is centered around our Goblint static analyzer for (multi-threaded) C programs. Since we don’t (widely) teach program analysis or OCaml, these topics require some learning but only about specific parts of Goblint. These are a good step if you’re interested in continuing with a MSc degree and getting deeper into program analysis.

BSc: (These are described in English because Goblint research and development are in English, but BSc theses are usually still written in Estonian.)

  1. Early Destabilization in the Top-Down Constraint Solver. Goblint uses side-effecting constraint systems and the TD3 solver to analyze multi-threaded programs. This solver has an inefficiency: it keeps computing things which it knows have to be recomputed. The goal of this thesis is to avoid this by introducing early destabilization which hopefully can speed up Goblint. It requires OCaml programming and understanding of the TD3 solver.
  2. Evaluating Side-Effecting Constraint System Solvers. Goblint analyzes multi-threaded programs using side-effecting constraint systems, which were introduced 22 years ago by Seidl, Vene and Müller-Olm. Many solvers have been proposed for these systems: naïve, worklist, SLR and TD3. They have been evaluated individually, but not against each other. The goal of this thesis is to compare them all experimentally and understand the differences. It requires OCaml programming and understanding of the solvers.
  3. Interrogation Testing of Goblint. Interrogation testing is a new method for testing program analyzers. It has been successfully used to find correctness and precision issues in a variety of analyzers, but it has not been applied to Goblint. The goal of this thesis is to interrogation test Goblint and fix simple found issues. It requires some understanding of abstract interpretation and possibly OCaml programming.
  4. 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 Goblint and integrate them into our Open Verification Dashboard. It requires OCaml programming and little knowledge of Goblint’s analyses.
  5. Alternative Control-Flow Graphs for Goblint. Goblint represents code-to-be-analyzed using control-flow graphs (CFGs). Sometimes they are too optimized for debugging, other times they may be too unoptimized for usability or performance. The goal of this thesis is to add alternative CFG constructions to Goblint. It requires OCaml programming.

MSc:

  1. Self-Refining Abstract Interpretation. Counterexample-guided abstraction refinement (CEGAR) is a general method for automatically improving the precision of program analysis by excluding impossible execution paths. One version currently implemented in Goblint is very limited and relies on an external SMT solver, another version relies on a symbolic executor. The goal of this thesis is to use abstract interpretation itself to identify impossible execution paths. It requires OCaml programming and understanding of abstract interpretation.
  2. Why Doesn’t Goblint Scale Up? Goblint uses abstract interpretation which is supposed to be fast. Although Goblint is quick on small and medium-sized programs, it does not scale so well to large real-world programs, which other abstract interpreters can handle. The goal of this thesis is to find out why and try to improve the scalability of Goblint. This requires profiling OCaml code and understanding of Goblint’s analyses.

Goblint-adjacent

Goblint is a decently-sized project which requires and uses various supporting software. These topics don’t involve OCaml programming and require less program analysis background knowledge, but still help the Goblint project as a whole.

BSc: (These are described in English because Goblint research and development are in English, but BSc theses are usually still written in Estonian.)

  1. Minimization for Octagon Abstract Domain in Apron. Goblint uses the Apron library for relational numeric analysis. Its octagon domain infers two-variable linear inequalities of the form ±x ± y ≤ c . The output from Apron is not very user-friendly: for large programs with many variables there are many redundant constraints which are implied by others. The goal of this thesis is to implement octagon minimization in Apron. It requires C programming and basic linear algebra.
  2. Verified Stack Abstractions. Goblint uses history-based thread IDs which are an abstraction of the stack data structure. The goal of this thesis is to formalize these thread IDs/stack abstractions and prove them correct. It requires proving in a proof assistant (e.g. Rocq, Lean).

SV-COMP

The Competition on Software Verification (SV-COMP) is an annual evaluation and comparison of the state of the art in program analysis. Its benchmark suite is the largest of its kind, containing over 33,000 C benchmarks. Goblint has participated in six editions of SV-COMP and I am involved in the organization of the competition.

BSc: (These are described in English because SV-COMP activities are in English, but BSc theses are usually still written in Estonian.)

  1. SV-COMP Benchmarks from Goblint Regression Tests. Goblint uses C programs with custom annotations as regression tests, but they are not directly suitable for SV-COMP. The goal of this thesis is to develop a robust automatic method for converting Goblint regression tests into SV-COMP benchmarks. It requires minimal knowledge of Goblint itself.
  2. Linter for Trivial SV-COMP Benchmarks. Among the thousands of benchmarks there are some which are trivial. For example, a single-threaded program cannot have a data race. Such benchmarks artificially inflate the benchmark suite, lowering its quality. The goal of this thesis is to implement a linter for detecting trivial SV-COMP benchmarks. It requires simple syntax analysis.
  3. SV-COMP Results Database. The results of SV-COMP are published as pretty HTML tables and raw XML files. Neither format is suitable for complex queries or statistical analysis. The goal of this thesis is to build a unified database containing the results of all 15 editions of SV-COMP. It requires SQL and data processing.
  4. Inferring Relationships Between Benchmarks. Different benchmarks in SV-COMP are often related in various ways. For example, a correct program might have multiple incorrect variants, or a difficult benchmark might have multiple easier variants. Unfortunately, these relationships are not systematically recorded. The goal of this thesis is to automatically infer such relationships from the benchmark suite itself.
Accept Cookies