Detail práce
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
statická analýza, analýza programů, abstraktní interpretace, Facebook Infer, porušení atomicity, paralelní programy, kontrakty pro souběžnost, atomické sekvence, atomicita, inkrementální analýza, modulární analýza, kompoziční analýza, interprocedurální analýza
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázku oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm "A".
- Diskutujte obtížnost rozšíření analyzátoru Atomer o podporu formálních parametrů funkcí a návratových hodnot.
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Honzík Jan M., prof. Ing., CSc. (UIFS FIT VUT), člen
Kořenek Jan, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
@bachelorsthesis{FITBT21689,
author = "Dominik Harmim",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "Statick\'{a} anal\'{y}za v n\'{a}stroji Facebook Infer zam\v{e}\v{r}en\'{a} na detekci poru\v{s}en\'{i} atomi\v{c}nosti",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2019,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/21689/"
}