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/"
}