et en

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