Lõputöö teema: Hulktahukate (teegi APRON) kasutamine Goblint analüsaatoris.

Goblint on staatiline programmianalüsaator C keele jaoks, mis keskendub andmejooksude tuvastamise ja andmejooksu-vabaduse tõestamisele. Lihtsustatult tähendab see seda, et Goblint saab kasutajalt sisendiks mitmelõimelise programmi lähtekoodi ja otsustab, kas kõik globaalsed muutujad on korrektselt lukkudega kaitstud.

Mida täpsemalt Goblint teab, milliseid väärtusi võivad (näiteks täisarvulised) muutujad omada, seda täpsem on kogu analüüsi tulemus ning seda vähem on ekslikke andmejooksude hoiatusi. Samas, liigne täpsus tähendab ka enamasti seda, et analüüs võtab ebamõistlikult kaua aega.

Üks huvitav viis arvulite muutujate väärtuste hulkade hoidmiseks on kumerad hulktahukad. Intuitiivselt tähendab see seda, et programmi seisundit mingis kohas kirjeldab teatav võrratuste süsteem. Näiteks, x>10, x<y+2 ning y<=20, kus x ja y on muutujad uuritavas C programmis.

APRON ongi siis selline teek, mis muuhulgas implementeerib kumerate hulktahukate arvutused ning mida on võrdlemisi lihtne Goblint analüsaatoris "tööle" saada. See tähendab seda, et esialgsed katsetused on sellega juba tehtud, kuid vaja oleks süstemaatiliselt kontrollida, kas kõik ikkagi tegelikult töötab. Vigade ilmnemisel tuleb Goblinti implementatsiooni, mis on OCaml keeles kirjutatud, täiendada.