Detail práce

Automata in Decision Procedures and Formal Verification

Disertační práce Student: Janků Petr Akademický rok: 2024/2025 Vedoucí: Holík Lukáš, doc. Mgr., Ph.D.
Název česky
Automaty v rozhodovacích procedurách a formální verifikaci
Jazyk práce
anglický
Abstrakt

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.

Klíčová slova

Ř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.

Ústav
Ústav inteligentních systémů FIT VUT v Brně
Studijní program
Výpočetní technika a informatika, obor Výpočetní technika a informatika
Soubory
Stav
obhájeno
Obhajoba
26. listopadu 2024
Citace
JANKŮ, Petr. Automata in Decision Procedures and Formal Verification. Brno, 2024. Disertační práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2024-11-26. Vedoucí práce Holík Lukáš. Dostupné z: https://www-dev.fit.vutbr.cz/study/phd-thesis/1508/
BibTeX 
@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/"
}

Závěrečné práce

Nahoru