Detail práce
Automata in Decision Procedures and Formal Verification
V této práci navrhneme rychlou redukci splnitelnosti formulí v straight-line a acyklickém fragmentu na problém prázdnosti alternujících konečných automatů (AFA), která je ve většině případů polynomiální. Tato redukce v kombinaci s pokročilými algoritmy pro kontrolu modelů, jako je IC3, poskytuje první praktický algoritmus pro řešení omezení nad řetězci zahrnujících konkatenaci, převodníky a regulární omezení. Dále zavedeme nový fragment řetězcových omezení zvaný chain-free a jeho relaxaci zvanou weakly chaninng spolu s rozhodovacími procedurami pro tyto fragmenty. Je důležité zmínit, že tyto nové fragmenty zobecňují jak straight-line fragment, tak acyklickou formu. Navíc představíme metodu pro ověření splnitelnosti omezení nad řetězci, zejména s převodem mezi řetězci a čísly, pomocí parametrických plochých automatů (PFA). Tento postup je doplněn o algoritmus pro převod omezení nad řetězci na lineární formule v polynomiálním čase s prohledávacím prostorem ohraničeným PFA. Na závěr navrhneme vylepšenou Parikhovu abstrakci pro řešení délkových omezení pro straight-line fragment.
Řešení řetězců, Střídavé konečné automaty, Rozhodovací procedura, IC3, Splnitelnost modulo teorií (SMT), Verifikace programů, Omezení řetězců, Automaty, Parikhův obraz.
@phdthesis{FITPT1508, author = "Petr Jank\r{u}", type = "Diserta\v{c}n\'{i} pr\'{a}ce", title = "Automata in Decision Procedures and Formal Verification", school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}", year = 2024, location = "Brno, CZ", language = "english", url = "https://www.fit.vut.cz/study/phd-thesis/1508/" }