et en

Danel Ahman

Efekte sisaldavate programmide verifitseerimine keeles F*

F* [1] on tõestustele orienteeritud sõltuvalt tüübitud programmeerimiskeel, mis toetab nii efektivabade kui arvutuslikke efekte (nt mälu ja sisent-väljundi kasutamine, erindite haldamine, mitte-deterministlike ja tõenäosuslike otsuste tegemine) sisaldavate programmide verifitseerimist. Lisaks võimaldab F* tõestatud koodi kompileerimist jooksutatavaks koodiks keeltes OCaml, C või Rust.

Lõputöö selles valdkonnas sisaldaks F* keele kasutamaõppimist ning tema efektisüsteemi (Dijkstra monaadide [2] ja kihiliste efektide [3]) kasutamist mõne efekte sisaldava programmitüki või algoritmi korrektsuse spetsifitseerimiseks ja verifitseerimiseks. Lõputöö üheks eesmärgiks oleks ka demonstreerida, et F* on hea tööriist hübriidseks verifitseerimiseks, kus F* keeles implementeeritakse ja tõestatakse ainult tarkvara kriitilised komponendid, samal ajal postuleerides ülejäänud kasutatavate teekide korrektsuse.

Näiteks, üks võimalik lõputöö projekt võiks sisaldada F*'i Steel ja Pulse'i raamistike [4] kasutamist IoT seadmetes kasutatava keeles C või Rust kirjutatud sardtarkvara korrektsuse verifitseerimiseks. Parema idee saamiseks projektis tehtavast tööst võib vaadata ühte varasemat eksperimenti [5], kus natuke vanemat Low* raamistikku kasutati lihtsa katkestustepõhise ESP32 mikrokontrolleril jooksva tarkvara mälukorrektsuse tõestamiseks.

Potentsiaalsed tudengid on alati oodatud ka omi ideid välja pakkuma, et millist efekte sisaldavat tarkvaratükki või algoritmi keeles F* verifitseerida. Tudengid kes on huvitatud algoritmide verifitseerimisest teistes sõltuvalt tüübitud programmeerimiskeeltes (nt Agda) on samuti oodatud ühendust võtma.

• [1] https://fstar-lang.org
• [2] https://arxiv.org/abs/1903.01237
• [3] https://www.fstar-lang.org/papers/indexedeffects/indexedeffects.pdf
• [4] https://fstar-lang.org/tutorial/book/pulse/pulse.html
• [5] https://github.com/danelahman/esp32-fstar

Asünkroonsed algebralised efektid

Asünkroonsed algebralised efektid [1,2] on lähenemine asünkroonsete arvutuste matemaatiliselt loomulikul moel lisamiseks programmeerimiskeeltesse, mis põhinevad või kasutavad algebralisi efekte ja nende haldureid [4]. See lähenemine on modelleeritud väikeses tuum lambda-arvutuses, millel on nii tüübi- ja efektisüsteem, operatsioonisemantika kui ka prototüüp implementatsioon [3].

Lõputöö selles valdkonnas sisaldaks näiteks kas ülalmainitud lambda-arvutuse metateoreetiliste omaduste uurimist (nt tema normaliseerimisomaduste uurimist) või ülalmainitud lambda-arvutuse ja prototüübi edasi arendamist (nt lisades tüübiteoreetilisi viise kuidas piirata protsessidevahelist kommunikatsiooni või lisades keelde üldised algebraliste efektide haldurid).

• [1] https://arxiv.org/abs/2003.02110
• [2] https://arxiv.org/abs/2307.13795
• [3] https://github.com/matijapretnar/aeff
• [4] https://homepages.inf.ed.ac.uk/slindley/papers/handlers.pdf

Ajalised ressursid

Ajalised ressursid [1] on lähenemine kuidas staatilist tüübisüsteemi kasutada selleks, et spetsifitseerida ja verifitseerida, et programmid oma käsutuses olevaid ressursse kasutaksid ajaliselt korrektselt. Näiteks koosterobotit programmeerides on vajalik, et teatud tegevused (nt mööbli kokkupanek) ei algaks liiga vara (pärast mööblitükkide värvimist). Sarnased näited on väga tavalised ka keemiliste lahuste ja protsessidega töötades.

Lõputöö selles valdkonnas sisaldaks ajaliste ressursside lähenemise aluseks oleva lambda-arvutuse laiendamist erinevatel uutel viisidel. Näiteks,

• lambda-arvutuse üldistamine, et oleks võimalik rääkida üldisematest spetsifikatsioonidest kui ainult ajalised piirangud (nt programmide jälgedest);
• lambda-arvutusse aeguvate ressursside lisamine;
• lambda-arvutusse alamtüüpimise ja -efektimise lisamine;
• ajaliste ressursside kombineerimine lineaarsete tüüpidega, et võimaldada lisaks ajalistele omadustele kirjeldada ka ressursside ruumilisi omadusi; või
• lambda-arvutusse ja tema modaalsesse tüübisüsteemi sõltuvate tüüpide lisamine.

Tudengid kellele meeldib rohkem programmeerida võivad selles valdkonnas lõputöö raames implementeerida ajaliste ressursside lähenemise aluseks oleva lambda-arvutuse jaoks prototüübi (kas eraldiseisva tüübikontrollija ja interpretaatori või DSLina keeles Haskell või OCaml) ja eksperimenteerida selle lähenemise edasiste näidetega.

• [1] https://arxiv.org/abs/2210.07738

Kontakt: Danel Ahman (danel.ahman@ut.ee)