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