23. aprillil kell 13.00 kaitseb Simmo Saan doktoritööd „Correctness Witnesses for Thread-Modular Program Analysis“ („Lõimeviisilise programmianalüüsi õigsustõendid”).
Juhendaja
kaasprof Vesal Vojdani, Tartu Ülikool
Oponendid
prof Patrick Cousot, New York University (USA)
prof Dirk Beyer, Müncheni Ludwig Maximiliani Ülikool (Saksamaa)
Kokkuvõte
Igaüks tahab, et tarkvara oleks kiire ja lihtsalt töötaks (korrektselt), st ei sisaldaks vigu. Mitmelõimelised programmid saavad olla efektiivsed, tehes mitut operatsiooni korraga, kuid neid võib olla keeruline korrektselt kirjutada. Kuna neid on ka keeruline testida, siis peab pöörduma formaalse verifitseerimise juurde. Seda on võimalik automatiseerida, kasutades staatilisi analüsaatoreid – teisi programme, mis üritavad automaatselt tarkvara verifitseerida. Automaatsed tarkvara verifitseerijad on aga ka ise keerukad programmid, mis võivad samuti olla vigased ja seeläbi anda ebakorrektseid tulemusi. Suurendamaks oma järelduste usaldusväärsust, võivad verifitseerijad luua tõendeid (ingl witnesses), mis paljastavad nende arutluskäigu analüüsitud programmi kohta. Sellised tõendusobjektid võimaldavad analüüsi tulemusi inspekteerida inimestel või isegi kolmandatel programmidel, mida nimetatakse tõendite valideerijateks. Kahjuks puudusid varem verifitseerimistõendid mitmelõimeliste programmide korrektsuse põhjendamiseks. Selle doktoritöö eesmärk ongi täita see uurimislünk ning kasutada tõendeid, et muuta mitmelõimeliste programmide analüüs usaldusväärseks, kuid ka kiireks ja täpseks.
Esiteks parandatakse selle töö raames mitmelõimeliste programmide analüüsi, kasutades abstraktset interpretatsiooni, mis on edukas meetod pärismaailma tarkvara verifitseerimiseks. Teiseks uuritake, kuidas abstraktne interpretatsioon võib kasu saada tõenditest, nii jõudluse kui ka täpsuse seisukohalt. Kolmandaks ühendatakse mainitud suunad ja pakutakse välja korrektsustõendid mitmelõimelistele programmidele, täites lõpuks uurimislünga. Kokkuvõttes edendatakse doktoritöös tipptasemel abstraktset interpretatsiooni ja verifitseerimistõendeid. Tõendid võimaldavad välja töötada paremaid staatilisi analüsaatoreid, mis omakorda aitavad tarkvaraarendajatel kirjutada korrektseid mitmelõimelisi programme.
