Kalmeri Apinis
Mingi algoritmi formaalne tõestamine Coq-is
Üks viis korrektse koodijupi saamiseks see genereerida Coq-i koodist, kus on võimaik korrektsust formaalselt tõestada. Kuna formaalne tõestamine on parajalt keerukas, ei saa lõputöö jaoks valida väga keerukat algoritmi. Baka tasemel pakun välja intervalli hulga aritmeetika ja magistri tasemel püsipunkti arvutamise kiirendamise algoritmi. Siin võiksite ka ise mingi algoritmi välja pakkuda.
Java baitkoodi staatiline analüüs
Uurimisrühmal on palju kogemusi C keele staatilise programmianalüüsiga. Nüüd soovime lisaks tegeleda ka Java maailma programmide analüüsiga. Programmi staatiline analüüs arvutab programmi koodi järgi selles kehtivaid invariante. Selle põhjal saab anda hinnanguid programmi (korrektsuse) kohta. See muidugi oleneb sellest, milliseid analüüse käivitatakse (ehk milliseid invariante otsitakse).
Abstraktse interpretatsiooni teooria järgi on staatiline programmianalüüs põhimõtteliselt lahendatud juba seitsmekümnendatel. Meie uurimisrühma liikmed on samuti 15 aastat kirjutanud programmianalüüsi temaatilisi teadusartikleid ja programme. Samas, praktilisi ja tavakasutajale sobivaid tööriistu praktiliselt ei eksisteeri.
Teemad
- võrrandisüsteemi lahendajate implementeerimine (teadusartiklite põhjal)
- relatsioonilise analüüsi tulemuse selgitamine (saab kirjutada teadusartikli)
Programmeerimskeelte kursuse uuendamine
Vanasti oli meil kursus nimega Programmeerimskeeled, kus õpetati erinevaid programmeerimiskeeli. Kuna see oli informaatika õppekavas kohustuslik, ei saanud seal huvitavamaid probleeme vaadata ja õpetatu jäi algse tutoriali tasemele. Niisiis, kui te armastatemingit programmeerimiskeelt (näiteks Rust), siis võiksite teha õppematerjali ja ülesanded selle kohta nii, et see näitaks selle keele tugevaid külgi. Kui saame kokku piisaval hulgal õppematerjale, saame sellest teha ametliku kursuse.
Kontakt: Kalmer Apinis (kalmer.apinis@ut.ee)
Tehtud lõputööd
- 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