Detail práce
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
V této práci se zabýváme regulárním model checkingem, což je technika pro analýzu programů, jejíchž stavový prostor může být nekonečný v důsledku práce například s neomezenými frontami, parametry, dynamicky propojenými datovými strukturami, rekurzivními procedurami nebo řetězci. Cílem této práce bylo implementovat vylepšení stávajícího prototypu nástroje ASMA implementujícího regulárním model checking nad knihovnou Automata of Microsoftu. Provedli jsme analýzu zdrojového kódu nástroje ASMA a zopakovaly analýzy všech dostupných srovnávacích programů. Identifikovali jsme některá úzká místa a několik z nich jsme vyřešili. Zejména jsme integrovali knihovnu obsahující další redukční algoritmy do nástroje ASMA, vytvořili několik nových verzí operace reverzní konkatenace, která se v benchmarcích ukázala jako velmi nákladná, vylepšili rozhraní příkazového řádku ASMA a implementovali některé další optimalizace. Výpočetní čas se při analýze větších programů snížil o 90 %.
regulární model checking, RMC, abstraktní regulární model checking, ARMC, konečné automaty, převodníky, symbolické konečné automaty, AutomataDotNet, ASMA, VeriFIT, reverzní konkatenace
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.
- Jaké je srovnání velikosti automatu získaných pomocí determinizace a minimalizace a redukovaných pomocí simulace/bisimulace?
- Jaké jsou další plány s použitím simulace pro redukci automatů v nástroji ASMA? Bude zcela zahozena na úkor determinizace a minimalizace?
- Jakým způsobem plánujete využít v nástroji zmiňované antichainy?
- Jaké jsou další plány s nástrojem ASMA?
- Jak se nástroj ASMA srovná s jinými nástroji pro analýzu programů s řetězci?
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Martínek Tomáš, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT), člen
@bachelorsthesis{FITBT25149,
author = "Martin Kmenta",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2022,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/25149/"
}