et en

Kalmer Apinis

Mingi algoritmi formaalne tõestamine Rocq-is

Üks viis korrektse koodijupi saamiseks see genereerida Rocq-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.

Teine variant oleks jätkata Kadi Sammuli tööd ja tõestada midagi seoses meie PRG projektiga. Sellisel juhul oleks kõne all maksta ka stipendiumi.

Teemad

  • tõestada oma valitud algoritm
  • viia praktiliseks Push-Relabel algoritmi implementatsioon
  • tõestada midagi seoses võrrandisüsteemide lahendajatega

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.

Kuna see teema on seotud meie PRG projektiga, siis saame nende teemade puhul arutada stipendiumi maksmist.

Teemad

  • võrrandisüsteemi lahendajate implementeerimine (teadusartiklite põhjal)
  • relatsioonilise analüüsi tulemuse selgitamine (saab kirjutada teadusartikli)
  • mäluanalüüsi integreerimine süsteemi
  • Põder analüsaatori parandamine, et võistelda SV-COMP'l
  • Põder analüsaatori parandamine

Õ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.

Lisaks on võimalus täiendada FP õpikut.

Teemad

  • projektitööd õppematerjalide loomine kursusele FP
  • mingi muu teema, mis teeb FP kursust paremaks
  • FP õpiku jaoks ülesannete valmistamine
  • FP õpiku lisapeatükid --- OCaml, Elm, Haskell

Funktsionaalne programmeerimine

Teame, et FP on teoorias tore. Aga kas seda on ka tegelikult tore kasutada? Selliste mõtete uurimiseks oleme nõus juhendama teie toodud ülesande, kui selle lahendamine kasutab FP-d piisavalt suures mahus.

Teemad

  • Teie toodud probleemi lahendamine mõne uue FP lahendusega (näiteks Elm või Elixir)
  • Teie toodud probleemi lahendamine mõne klassikalise FP lahendusega (näiteks Haskell või Ocaml)

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

Tehtud lõputööd