et en

Kalmer 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. Hea oleks, kui keegi jätkaks Aksel Õim-i tööd ja looks praktiliselt kasutatava korrektse Push-Relabel algoritmi implementatsiooni. Siin võite ka ise oma lemmikalgoritmi 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)
  • Põder analüsaatori parandamine, et võistelda SV-COMP'l

Õppematerjalid Funktsionaalprogrammeerimise jaoks

Siin on palju erinevaid võimalusi, millest alustada, aga lõppkokkuvõttes tahame FP kursuse jaoks saada juurde kvaliteetseid, sisukaid ja väljakutset pakkuvaid ülesandeid. Näiteks tõlkida mingi reaktiivse programmeerimise lahendus Haskellist Idrisesse, uurida/lahendada mingit andmeteaduse tüüpprobleemi Idrises või uurida mingit huvitavat algoritmi.

Kontakt: Kalmer Apinis (kalmer.apinis@ut.ee)

Tehtud lõputööd