An Automata-Based Decision Procedure

Název česky

Rozhodovací procedura založená na automatech

Jazyk práce

anglický

Abstrakt

Presburgerova aritmetika (PrA) je rozhodnutelná teorie přirozených čísel prvního řádu, která nachází uplatnění v mnoha oblastech formální verifikace vlastností softwaru. Řešiče SMT nástroje implementující různé algoritmické přístupy k rozhodování, zda má formule řešení hrají ve formální verifikaci klíčovou roli. V této práci dokumentujeme vytvoření nového automatického SMT řešiče pro PrA založeného na konečných automatech přístupu, který v současnosti žádný SMT řešič nepoužívá. Uvádíme přehled výzev a jejich řešení vyplývajících ze složitosti takového nástroje, včetně výsledků z provedených experimentů, které již identifikují problémy, kde tento alternativní přístup překonává nejmodernější řešiče. Uvádíme také identifikované problémy, u nichž výkonnost postupu založeného na automatech naráží na problémy, které představují otevřené možnosti výzkumu.

Klíčová slova

Presburgerova aritmetika, SMT solver, Celočíselná lineárna aritmetika, Konečný automat

Ústav

Ústav inteligentních systémů FIT VUT v Brně

Studijní program

Informační technologie

Soubory

Stav

obhájeno, hodnocení A

Obhajoba

13. června 2022

Oponent

Češka Milan, doc. RNDr., Ph.D.

Průběh obhajoby

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.

Otázky u obhajoby

1) Můžete vysvětlit proč je na uvedeném Frobeniově problému Vaše řešení výrazně lepší než nástroje Z3 či CVC5?

2) Očekáváte, že existují jiné (prakticky relevantní problémy), kde budete rovněž dosahovat lepších výsledků něž Z3 či CVC5?

Komise

Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT), předseda
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

Citace

HEČKO, Michal. An Automata-Based Decision Procedure. Brno, 2022. Bakalářská práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2022-06-13. Vedoucí práce Lengál Ondřej. Dostupné z: https://www.fit.vut.cz/study/thesis/24744/

BibTeX

@bachelorsthesis{FITBT24744,
    author = "Michal He\v{c}ko",
    type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
    title = "An Automata-Based Decision Procedure",
    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/24744/"
}