Kalmeri Apinis
Formally proving some algorithm in Coq
One way to produce a correct software module is to generate it from Coq code, where you can formally prove correctness. As formal proofs are difficult, we cannot choose a very complicated algorithm. For the bachelor level, I propose implementing interval set arithmetic, and for the master level, acceleration of fixpoint calculation. You may propose your own algorithm.
Static analysis of Java bytecode
We have a lot of experience doing static analysis of C programs. Now we want to also analyse programs in the Java world. Static analysis computes invariants based on the source code and the invariants can be used to assess the correctness of programs. This of course depends on the analysis --- which kinds of invariants can be detected.
Abstract interpretation theoretically solved static analysis already in the seventies. Our group also has been writing analysers and research papers for 15 years. But still there are no practically usable analysis tools which do no require expert knowledge.
Topics
- implementation ofa a constraint system solver (based on a paper)
- explaining a relational analysis (possible to write a paper)
Programming language course
We used to have a course called Programming Languages, where we taught different programming languages. As it was mandatory for informatics students, we did not get to any interesting topics. If you love a programming language (such as Rust) then why not develop some course materials for us such that it displays the strengths of that language. If we collect enough teaching materials for different languges, we can create a real course out of them.
Contact for more info: Kalmer Apinis (kalmer.apinis@ut.ee)
Completed theses
- Maarika Markus, "Veebirakendus funktsionaalprogrammeerimise ja -keele Idris õppimiseks", 2022
- Karoliine Holter, "Funktsionaalprogrammeerimise õpetamine Idrises ", 2021
- Peter Kallaste, "Efektisüsteemide õpetamine Haskellis", 2021
- Karl Marten Mägi, "Modulaarne staatiline programmianalüüs", 2021
- Halliki Mullari, "Java baitkoodi sünkroniseerimise analüüs raamistikus Põder", 2020
- Liem Radita Tapaning Hesti, "Autotööstuse tarkvara mudelipõhine arendamine ja analüüs", 2019
- Raul Redpap, "Kahni algoritmi tõestamine Coq raamistikus", 2019
- Mirjam Iher, "Nõrgima eeltingimuse staatiline analüüs pinukeeltele", 2019
- Andre Sinisalu, "Java programmide staatiline intervallanalüüs raamistikus Põder", 2019
- Simmo Saan, "Abstraktsete domeenide omaduspõhine testimine", 2018
- Liisi Kerik, " Funktsionaalse programmeerimiskeele liigisüsteem", 2018
- Tenno Veber, "Haskelli FRP teegi uurimine: Reactive-banana", 2017
- Karl-Martin Uiga, "Tüübiohutu FRP teegi uurimine: Grapefruit", 2017
- Kaarel Tinn, "Veebirakenduse loomine funktsionaalses programmeerimiskeeles Elixir", 2017
- Marti Mutso, "Haxl teegi uurimine", 2017
- Margus Pollmann, "Haskelli teegi Euterpea uurimine", 2017
- Sebastian Wiesner, "Implementing Widening as an Abstract Domain", 2014
- Stefan Dangl, "State space reduction by injecting external invariants into the internal program representation of Goblint"
- Yannick Scherer, "Signed agnostic interval analysis for Gobint", 2013