{"id":15,"date":"2025-07-02T15:07:08","date_gmt":"2025-07-02T12:07:08","guid":{"rendered":"https:\/\/sisu.ut.ee\/sws\/?page_id=15"},"modified":"2026-02-24T19:54:23","modified_gmt":"2026-02-24T17:54:23","slug":"thesis-topics","status":"publish","type":"page","link":"https:\/\/sisu.ut.ee\/sws\/thesis-topics\/","title":{"rendered":"Thesis Topics"},"content":{"rendered":"<p>We supervise topics related to programming languages and verification. Ambitious students, especially those interested in potential Ph.D. positions, should first familiarize themselves with our\u00a0<a href=\"https:\/\/sws.cs.ut.ee\/Main\/PRGTopics\">Explainable Verification<\/a>\u00a0overview.<\/p>\n\n\n\n<p><em>Click on the names of individual supervisors to see their proposed topics.<\/em><\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/sws.cs.ut.ee\/Main\/VesalThesis\">Vesal Vojdani<\/a>: Explainable verification, AKT and Software Security course material.<\/li>\n\n\n\n<li><a href=\"https:\/\/plas.cs.ut.ee\/Teemad\/Ahman\">Danel Ahman<\/a>: Algebraic effects, Asynchrony, Temporal resources, F*, Agda, Logic in Computer Science course.<\/li>\n\n\n\n<li><a href=\"https:\/\/sws.cs.ut.ee\/Teemad\/Apinis\">Kalmer Apinis<\/a>: Functional programming, Program Analysis, the Rocq Prover.<\/li>\n\n\n\n<li><a href=\"https:\/\/kodu.ut.ee\/~nester\/thesis-topics.html\">Chad Nester<\/a>: Category Theory, Programming Language Semantics, Logic<\/li>\n\n\n\n<li><a href=\"https:\/\/sws.cs.ut.ee\/Main\/SimmoThesis\">Simmo Saan<\/a>: Goblint, Compiler construction course.<\/li>\n\n\n\n<li><a href=\"https:\/\/plas.cs.ut.ee\/Teemad\/Rucy\">Bruno Carneiro<\/a>: Query Optimisation, Ontologies, Logic Programming.<\/li>\n<\/ul>\n\n\n\n<div style=\"height:25px\" aria-hidden=\"true\" class=\"wp-block-spacer\"><\/div>\n\n\n\n<p>We develop and aim to maintain some useful experimental tools and languages. If you want to work on something more concrete, you may benefit from our (vast ocean of) knowledge while contributing to one of our pet projects:<\/p>\n\n\n\n<figure class=\"wp-block-image alignright size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"960\" height=\"720\" src=\"https:\/\/sisu.ut.ee\/wp-content\/uploads\/sites\/920\/wettlaufweltmeister.svg\" alt=\"\" class=\"wp-image-16\"><\/figure>\n\n\n\n<h2 class=\"wp-block-heading\">Goblint: Race Detection World Champion<\/h2>\n\n\n\n<p><a href=\"https:\/\/goblint.in.tum.de\/\">Goblint<\/a>\u00a0is a static analyzer written in OCaml for the analysis of multi-threaded C programs. Goblint is developed jointly with the\u00a0<a href=\"https:\/\/www.cs.cit.tum.de\/en\/pl\/home\/\">Technical University of Munich<\/a>. This is a very exciting and lively project, so we encourage our best students to use this opportunity to collaborate with the\u00a0<em>Cr\u00e8me de la Cr\u00e8me<\/em>\u00a0of European computer science.<\/p>\n\n\n\n<p><em>Contacts:\u00a0<a href=\"https:\/\/sws.cs.ut.ee\/Main\/SimmoThesis#goblint\">Simmo Saan<\/a>,\u00a0<a href=\"https:\/\/sws.cs.ut.ee\/Main\/VesalThesis\">Vesal Vojdani<\/a><\/em>.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">P\u00f5der: Towards Explainable Static Analysis<\/h2>\n\n\n\n<p><a href=\"https:\/\/bitbucket.org\/kalmera\/poder\">P\u00f5der<\/a>\u00a0is 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\u2019s functionality in P\u00f5der or proceed to certify these algorithms in Coq. It may be helpful to draw inspiration from the\u00a0<a href=\"https:\/\/iris-project.org\/\">Iris framework<\/a>\u00a0where similar results are proven.<\/p>\n\n\n\n<p><em>Contact:\u00a0<a href=\"https:\/\/plas.cs.ut.ee\/Teemad\/Apinis\">Kalmer Apinis<\/a><\/em>.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Temporal Millet: Modal Types for Temporal Effects<\/h2>\n\n\n\n<p><a href=\"https:\/\/github.com\/danelahman\/temporal-millet\">Temporal Millet<\/a>\u00a0is a prototype programming language that combines modal types with graded effect systems to specify and verify temporal properties of program resources, with automatic checking via Hindley-Milner style type inference. It extends Matija Pretnar\u2019s Millet with temporal algebraic effects and effect handlers whose operations are guaranteed to respect their declared time costs. A\u00a0<a href=\"https:\/\/danel.ahman.ee\/temporal-millet\/\">web UI<\/a>\u00a0is provided for demonstrating reductions.<\/p>\n\n\n\n<p><em>Contact:\u00a0<a href=\"https:\/\/plas.cs.ut.ee\/Teemad\/Ahman\">Danel Ahman<\/a><\/em>.<\/p>\n\n\n\n<p><\/p>\n\n\n\n<p><\/p>\n","protected":false},"excerpt":{"rendered":"<p>We supervise topics related to programming languages and verification. Ambitious students, especially those interested in potential Ph.D. positions, should first familiarize themselves with our\u00a0Explainable Verification\u00a0overview. Click on the names of individual supervisors to see their proposed topics. We develop and &#8230;<\/p>\n","protected":false},"author":819,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-15","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/sisu.ut.ee\/sws\/wp-json\/wp\/v2\/pages\/15","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/sisu.ut.ee\/sws\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/sisu.ut.ee\/sws\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/sisu.ut.ee\/sws\/wp-json\/wp\/v2\/users\/819"}],"replies":[{"embeddable":true,"href":"https:\/\/sisu.ut.ee\/sws\/wp-json\/wp\/v2\/comments?post=15"}],"version-history":[{"count":4,"href":"https:\/\/sisu.ut.ee\/sws\/wp-json\/wp\/v2\/pages\/15\/revisions"}],"predecessor-version":[{"id":94,"href":"https:\/\/sisu.ut.ee\/sws\/wp-json\/wp\/v2\/pages\/15\/revisions\/94"}],"wp:attachment":[{"href":"https:\/\/sisu.ut.ee\/sws\/wp-json\/wp\/v2\/media?parent=15"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}