Detail práce
Verifikace programů s ukazateli založená na detekci vzorů
Tato práce navazuje na výsledky studií v oblasti verifikace nekonečně stavových systémů. Konkrétně se jedná o oblast abstraktního model checkingu. Seznámili jsme se s metodou založenou na abstrakci paměťové konfigurace pomocí paměťových vzorů. Tato metoda byla navržena pro verifikaci programů pracujících s dynamickými paměťovými strukturami jako například seznamy. Na dynamické paměťové struktury je nahlíženo jako na orientované grafy. Verifikace na základě paměťových vzorů abstrahuje obecně libovolné množství vytvořených uzlů do jednoho sumarizovaného uzlu. Tím se dosáhne reprezentace obecně neukončeného grafu konečným zápisem. Poté je možno efektivně provést verifikaci nad tímto abstrahovaným grafem. V naší práci se zabýváme tvorbou modelu pro nástroj implementující verifikaci na základě paměťových vzorů. Model programu je vytvořen z podmnožiny jazyka C. Hlavním přínosem práce je automatizace tvorby modelu pro verifikaci a tím dosáhnutí úplné automatizovanosti procesu verifikace. Je tak možné verifikovat programy napsané v běžném programovacím jazyce. V této práci je diskutována syntaxe vstupního jazyka i implementační detaily překladu.
systém, verifikace, formální verifikace, verifikace na základě paměťových vzorů, dynamická paměťová struktura, vzor, sumarizace, materializace, model, nadaproximace, nedeterminismus, jazyk C
Herout Pavel, doc. Ing., Ph.D. (ZČU v Plzni), člen
Lukáš Roman, Ing., Ph.D. (UIFS FIT VUT), člen
Růžička Richard, doc. Ing., Ph.D., MBA (UPSY FIT VUT), člen
Strnadel Josef, Ing., Ph.D. (UPSY FIT VUT), člen
Zbořil František, doc. Ing., Ph.D. (UITS FIT VUT), člen
@bachelorsthesis{FITBT5406, author = "Jan Kub\'{i}\v{c}ek", type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce", title = "Verifikace program\r{u} s ukazateli zalo\v{z}en\'{a} na detekci vzor\r{u}", school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}", year = 2007, location = "Brno, CZ", language = "czech", url = "https://www.fit.vut.cz/study/thesis/5406/" }