Detail práce
Překladač grafu toků dat do logiky bitových vektorů
Cílem této bakalářské práce je vytvořit a implementovat nástroj pro překlad modelů grafů toků dat do formátu SMT-LIB.Práce navazuje na projekt HADES výzkumné skupiny VeriFIT Fakulty informačních technologií Vysokého učení technického v Brně.V řešení bylo použito překladače vytvářejícího z původního grafu objektový model. Objektový model je možné převést do zápisu ve formátu SMT-LIB a přidat do něj aserce požadovaných vlastností systému. Pro ověřování vlastností závisejících na změnách systému je použita metoda rozbalování smyček s uživatelem zadanou hranicí maximálního počtu rozbalení.Možnosti vytvořeného nástoje jsou demonstrovány na sadě modelů grafů toků dat pokrývající všechny prvky vstupního jazyka VAM a jejich kombinace.Výsledek této práce představuje nové možnosti pro zpracování grafů toků dat ve formátu VAM a jejich verifikaci.
Formální verifikace, SMT, grafy toků dat, VAM, překladače
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.
- Zkoušel jste porovnávat různé způsoby převodu grafů toku dat na formule SMT? Jaké jsou rozdíly?
- Existují jiné přístupy pro detekci hazardů pomocí převodu do SMT?
Burget Lukáš, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Jaroš Jiří, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Křivka Zbyněk, Ing., Ph.D. (UIFS FIT VUT), člen
@bachelorsthesis{FITBT18543,
author = "Tom\'{a}\v{s} Su\v{s}ovsk\'{y}",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "P\v{r}eklada\v{c} grafu tok\r{u} dat do logiky bitov\'{y}ch vektor\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 = 2016,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/18543/"
}