Detail práce
Vizualizace datových struktur pro verifikační nástroje
Cílem práce je objektově orientovaný návrh a implementace knihovny, která poskytne verifikačnímu nástroji Predator a dalším nástrojům jednotné rozhraní pro vizualizaci interních datových struktur především pro účely jejich ladění. Práce analyzuje některé vlastnosti verifikačních nástrojů Predator, Forester a CPAchecker. Knihovna poskytuje nejen grafický, ale také textový výstup ve formátu jazyka DOT. Výsledek byl otestován připojením knihovny k verifikačnímu nástroji Predator.
Verifikace, Vizualizace datových struktur, Verifikační nástroj, Predator, Forester, CPAchecker
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 C.
- Můžete shrnout jaké výhody pro verifikační nástroje (mimo nástroje Predator) poskytuje použití vámi vytvořené knihovny oproti přímému napojení na funkce Graphvizu?
Bartík Vladimír, Ing., Ph.D. (UIFS FIT VUT), člen
Burget Lukáš, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
Strnadel Josef, Ing., Ph.D. (UPSY FIT VUT), člen
@bachelorsthesis{FITBT18837, author = "Michael Holubec", type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce", title = "Vizualizace datov\'{y}ch struktur pro verifika\v{c}n\'{i} n\'{a}stroje", school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}", year = 2016, location = "Brno, CZ", language = "czech", url = "https://www.fit.vut.cz/study/thesis/18837/" }