arvutiteaduse instituudi lõputööderegister


Andmevooanalüüsi tõestusobjektide loomine
Nimi Simmo Saan
Kokkuvõte Programmianalüsaator, mis määrab, kas antud programm rahuldab või rikub spetsifikatsiooni, võib ise sisaldada vigu ja seega olla ebausaldusväärne. Seepärast peaks analüsaator tõendama oma väiteid tõestusobjektidega (ingl. witness), mis on arusaadavad programmeerijale ja automaatselt kontrollitavad sõltumatute tööriistadega. Protseduuridevaheline andmevooanalüüs sobib hästi teatud probleemide lahendamiseks, aga selle abstraktsioonid otseselt ei vasta nõutud tõestusobjektidele. Töös näidatakse, et andmevooanalüüsiga saab tõestusobjekte luua, disainides vajalikud meetodid, millega käsitleda protseduuridevahelisust, ja kohandatakse võte mudelkontrollist, et suurendada loodud tõestusobjektide täpsust. Ideed implementeeritakse ja eksperimentaalselt testitakse andmevooanalüsaatoris Goblint. See võimaldab suurendada andmevooanalüsaatorite usaldusväärtust ja kasutatavust ning lubab neid võrrelda teiste verifitseerijatega.
Lõputöö keel inglise
Lõputöö tüüp Magister - Informaatika
Juhendaja(d) Vesal Vojdani
Kaitsmise aasta 2020
PDF