Skip to content

Laboratory for Software Science

Thesis topics from Vesal Vojdani

I have a significant amount of commitments in fall, so I have to focus on supervising work that falls within the scope of our Explainable Verification grant. Ambitious students should read the grant overview, identify an interesting topic area, look at the cited papers, and come discuss with potential topics with us. Unfortunately, most of you are hopelessly lazy, and want to be spoon fed a clear topic, so I will provide some examples here.

The topics below are formulated as MSc topics; ambitious bachelor students may also try them, with a smaller scope that we agree on together. For each topic we have already run a small proof of concept, so you start from working code and know what did not work. Ask for the full description of a topic.

AI and Program Analysis

Language models proposing what a sound analyzer then checks, and sound analysis applied to neural networks. Where a topic uses a language model, we are interested in small open models that run on a laptop, not in expensive hosted services.

  1. Calibrated Prediction of Program Safety for Inconclusive Static Analysis Results. When Goblint cannot decide a program, a model could predict whether it is actually safe; a first attempt shows how easily such results are overstated. The goal of this thesis is to evaluate such predictions honestly, with calibration on programs unlike those the model was trained on. It will be co-supervised from machine learning.
  2. Language Models as Untrusted Oracles for a Sound Static Analyzer. A model proposes configurations, annotations or library specifications for Goblint, and nothing it says is trusted until Goblint has checked it; in a first experiment an agent resolved 8 of 9 false alarms and silenced no real bug. The goal of this thesis is to measure when this helps and when it is unsafe.
  3. Synthesis of Sound Abstract Transformers with Small Language Models. Many of Goblint’s abstract operators are less precise than they could be. The goal of this thesis is to let a small model propose more precise operators and accept only those that pass an exhaustive or SMT soundness check, in the spirit of SAIL.
  4. Fairness Certification of Neural Networks by Abstract Interpretation: Replication and Checkable Certificates. Urban et al. (OOPSLA 2020) use abstract interpretation to prove that a classifier’s decision does not depend on a feature such as gender or age; we have rebuilt their tool Libra and rerun part of the experiments. The guarantee is for real-number arithmetic while the network runs in floating point, and the result cannot be checked without rerunning the tool. The goal of this thesis is to replicate and evaluate the approach and to make its result a checkable certificate.

Mechanized Proofs in Lean

Our analyses come with pen-and-paper soundness arguments. These topics state and prove them in a proof assistant, where the hard part is choosing a statement that really describes the analyzer.

  1. Mechanized Soundness and Optimality of Goblint’s Bitfield Domain in Lean. The bitfield domain tracks which bits of an integer may be 0 or 1. The goal of this thesis is to prove in Lean 4 that its operators are sound and as precise as possible for every bit width, and that the proofs are about Goblint’s actual OCaml code; the bitwise operators are already done, arithmetic and shifts are open (compare Rocq Bottom).
  2. Mechanized Soundness of a Lockset-Based Race Analysis in Lean. A first Lean proof shows that a lockset-based race analysis like Goblint’s is sound for programs with branches and loops. The goal of this thesis is to extend it towards the full analysis and its newer digest framework, and to argue that the model is faithful to Goblint.
  3. Mechanized Correctness of Goblint’s Fixpoint Solvers in Lean. Goblint computes its results with a fixpoint solver, which was recently parallelized. The goal of this thesis is to prove in Lean that the parallel solver returns a correct solution, including widening; alternatively, to recast the simple and incremental top-down solvers in Lean, continuing Tilscher et al. 2023.

Soundness of Goblint

These topics make explicit what Goblint has shown when it says a program is safe, and under which assumptions: by testing them, by proving them, or by exporting them as evidence that another tool can check.

  1. Soundness and Precision Contracts for Goblint’s Integer Domains. Goblint’s integer domains have dozens of hand-written abstract operators, and nothing says which C semantics each one implements; our test harness found four unsound operators that the unit tests miss. The goal of this thesis is to write down the contract of each operator together with the Goblint maintainers, classify every deviation, and check the combination of domains, where one domain can hide another’s unsoundness (as in the eBPF verifier).
  2. Sound Race Analysis of Per-Thread Array Cells in Goblint. Sound race verifiers fail when each thread writes its own cell of a shared array (Holter et al. 2025); a prototype already handles a fixed number of threads. The goal of this thesis is to handle threads created in a loop, in the spirit of how we verified arrays of locks, and to argue why it is sound.
  3. Verification Witnesses as Evidence for VEX Non-Exploitability Claims. Software vendors state that a known vulnerability does not affect their product because the vulnerable code is unreachable (VEX), and nothing checks such claims. The goal of this thesis is to bind such a statement to a machine-checkable witness from a sound analyzer.
  4. Termination Analysis and Termination Witnesses in Goblint. Goblint gives up on many terminating programs because of a crude test for backward jumps; a small patch already recovers proofs for 64 of 87 such benchmark tasks. The goal of this thesis is to make the termination argument explicit and to export it as a termination witness that independent validators such as CPAchecker can check.
  5. Reporting the Proved Results of a Sound Analyzer Together with Their Assumptions. A sound analyzer’s “verified” usually rests on assumptions that its reports do not show. The goal of this thesis is to get Goblint’s proved results and their assumptions into the standard report format (SARIF) and the Open Verification Dashboard.
  6. Confirming and Refuting Static Analysis Alarms with Sanitizers and Test Generation. A warning of a sound analyzer may be a real bug or a false alarm. The goal of this thesis is to classify each warning as confirmed (an input that triggers the bug), refuted or unknown, using sanitizers and test generation, and to find out why the rest stay unknown; a first pipeline confirms 7 of 10 alarms.

User Studies

These topics study how people read and use what analysis tools report, through experiments with people and, in the last one, a tool built for them.

  1. Interpreting the Output of a Sound Static Analyzer: A User Study. People reading a sound analyzer’s output have to tell real bugs from false alarms, and to decide what a missing warning means. The goal of this thesis is to run a study with stimuli from real Goblint runs (they and a task page already exist), following studies such as Kaleeswaran et al. 2023.
  2. Overreliance on Language Model Explanations in Static Analysis Alarm Triage: A User Study. A language model can explain a warning, but its explanation may be wrong. The goal of this thesis is to find out whether such explanations make people better at triaging alarms, or make them trust wrong ones; a labelled corpus of 54 Goblint alarms exists.
  3. Visualizing Synchronization Traces to Find Concurrency Hotspots in C/C++ Programs. Our lab has a ThreadSanitizer-compatible runtime that records the synchronization events of a C/C++ program run: atomic operations, lock calls and which thread synchronized with which. The goal of this thesis is to design and build a viewer that lets a developer find contended locks, retrying compare-and-swap loops and other hotspots in such a trace, and to evaluate it with users. Proposed by Jevgenijs Protopopovs, who develops the runtime.

Estonian BSc Topics

AKT ainega seotud teemad. Me plaanime seoses uute Java versioonide ja tehisintellektiga aines suhtesliselt suuri muudatusi. Seetõttu oleks siin võimalik pakkuda uusi teemasid, et välja töötada õppematerjale, mis tooksid rohkem rohkem esile tarkvara modelleerimise ja spetsifitseerimise võimalusi. Meie täpsemad plaanid selguvad paari nädala pärast. Endiselt on võimalik uurida ka järgmisi teemasid:

  • Eetikatestide uurimine ja arendamine
  • AKT keelest LLVM baitkoodi genereerimine
  • CMa simulaatori (VAM) veebiversiooni loomine
  • AKT keelele lisada turvalise andmevoo tüübid
  • Erinevad silmaringimaterjalid AKT või Tarkvara turvalisuse kursuse jaoks: automaatverifitseerijate demode loomine. AKT keele jaoks implementeerida lihtsustatud versioon SV-COMP töövahenditest:
Accept Cookies