Kalmeri Apinis

Interaktiivse teoreemitõestuse kursuse õppematerjalid

Loomulik järgmine samm peale puhast ja laiska funktsionaalset keelt (Haskelli) on sõltuvate tüüpidega keel. Coq-i tüübisüsteem on nimelt nii võimas, et programmi korrektsuse tingimuse saab kodeerida programmi tüüpi. S.t iga programm, mis kompileerub on automaatselt korrektne.

Interaktiivse teoreemitõestuse kursuses vaatame esmalt, kuidas käib lihtsate matemaatiliste tingimuste spetsifitseerimine ja tõestamine Coq keeles. Õpitud oskusi saab kasutada (ja mingil määral kasutamegi) programmide korrektsuse üle arutlemiseks. Kursust on ühel korral juba loetud; olemas on hulk ülesandeid. Vaja oleks luua õppematerjalid ja struktureerida ülesanded, et tudengid jõuaksid kursuses kaugemale --- põnevamate teemadeni.

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.

Selle projektikga püüame uurida, miks eelnevad programmid polnud edukad just kasutatavuse suhtes. Teeme lõpuks ühe kasutatava staatilise analüsaatori!

Tegemist on keerulise ettevõtmisega, millega hakkame tegelema ka siis, kui ükski tudeng selle vastu huvi ei tunne. Tule kampa!

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

Tehtud lõputööd