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.

English MSc Topics

Verifying a simple incremental solver in Lean. You would begin with familiarizing yourself with the existing work in verifying our solvers (Seidl et al. 2023) and recast those simple solvers in Lean. Then, take a simplified version of the incremental Top-Down solver (Seidl et al. 2020) and formalize these proofs. Then, familiarize yourself with Update Monads (Ahman and Uustalu 2013) to see if this helps in structuring the algorithm and proof.

Symbolic automated reasoning about unbounded threads. In previous work (Holter et al. 2025), we identified limitations in current approaches to data race verification. Eventually, we want address these challenges, so you could pick one and solve it! For example, consider the case where a bunch of threads are created in a loop and each thread is given an index where it (and only it) can write into a shared array. We know how to verify race freedom when each array element is protected by a lock in a corresponding array (Vojdani et al. 2016), so it should be possible to reason about threads created in a loop in similar ways, or maybe you have a better approach?

Neuro-Symbolic Software Understanding. Software understanding, as defined in the NSA joint statement is the "rigorous practice of constructing and assessing software-controlled systems to verify their functionality, safety, and security by design across all conditions—normal, abnormal, and hostile" and encompasses formal methods, artificial intelligence, threat modeling, game theory, and cognitive science. In particular, it would be interesting combine AI and our analysis approaches (think of AlphaProof). Low-hanging fruit would be to integrate goblint into LLM agents via the Model Context Protocol and compare with goblint alone or the LLM alone, but there are more topics possible here.

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: