Staatilise analüsaatori Goblinti regioonianalüüsi täiendamine aja partitsioneerimisega happens-before teabe alusel
Nimi
Vootele Rõtov
Kokkuvõte
Seadmedraiverite ehk ohjurite paralleelne olemus muudab
nendest vigade leidmise inimese jaoks väga keeruliseks. Staatiline analüsaator
Goblint üritab automaatselt verifitseerida, et ohjuris puuduvad andmejooksud.
Sealjuures on suureks väljakutseks analüüsi täpsus. Käesolev töö arendab edasi
Goblinti regioonianalüüsi, mis võimaldab arvesse võtta valdkonnale eriomaseid
happens-before tagatisi. Väljapakutud täienduse implementeerimise ning
muudatuste mõju analüüsimise aluseks on võetud Linuxi ohjurite alamhulk. Me
näitame, et mainitud edasiarendus suurendab Goblinti täpsust character tüüpi
ohjurite analüüsimisel.
nendest vigade leidmise inimese jaoks väga keeruliseks. Staatiline analüsaator
Goblint üritab automaatselt verifitseerida, et ohjuris puuduvad andmejooksud.
Sealjuures on suureks väljakutseks analüüsi täpsus. Käesolev töö arendab edasi
Goblinti regioonianalüüsi, mis võimaldab arvesse võtta valdkonnale eriomaseid
happens-before tagatisi. Väljapakutud täienduse implementeerimise ning
muudatuste mõju analüüsimise aluseks on võetud Linuxi ohjurite alamhulk. Me
näitame, et mainitud edasiarendus suurendab Goblinti täpsust character tüüpi
ohjurite analüüsimisel.
Lõputöö keel
inglise
Lõputöö tüüp
Magister - Informaatika
Juhendaja(d)
Vesal Vojdani, Kalmer Apinis
Kaitsmise aasta
2016