Detail práce
Static Analysis in the Frama-C Environment Focused on Deadlock Detection
Tato práce se zabývá návrhem nového statického analyzátoru pro detekci uváznutí, implementovaného jako plugin platformy Frama-C. Kromě samotného algoritmu pro detekci uváznutí představuje také odlehčené řešení, které umožňuje využít platformu Frama-C pro analýzu vícevláknových programů s využitím analyzátorů Frama-C podporujících pouze sekvenční programy. Výsledky experimentů ukazují, že implementovaný nástroj je schopný analyzovat reálné programy s vysokou přesností. Pro demonstraci další rozšiřitelnosti je představeno experimentální rozšíření umožňující detekovat také časově závislé chyby nad daty.
uváznutí, časově závislá chyba nad daty, statická analýza, abstraktní interpretace, analýza vícevláknových programů, Frama-C
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ázky 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.
- Je počet cest na hranách grafu omezený i v případě rekurzivních programů, kde je počet rekurzivních volání neomezený? Jak to?
- Existují možné alternativy k nástroji EVA, který by byly rychlejší/přesnější ... ?
- Jak by se dal Váš přístup smysluplně vylepšit co do efektivity, přesnosti nebo obecnosti?
Kekely Lukáš, Ing., Ph.D. (UPSY FIT VUT), člen
Křivka Zbyněk, Ing., Ph.D. (UIFS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Španěl Michal, doc. Ing., Ph.D. (UPGM FIT VUT), člen
@bachelorsthesis{FITBT22928, author = "Tom\'{a}\v{s} Dac\'{i}k", type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce", title = "Static Analysis in the Frama-C Environment Focused on Deadlock Detection", school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}", year = 2020, location = "Brno, CZ", language = "english", url = "https://www.fit.vut.cz/study/thesis/22928/" }