Detail práce
Automata in Infinite-state Formal Verification
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnýmistromy, a použití těchto automatů při formální verifikaci nekonečně stavovýchsystémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovýmistrukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
antiřetězce, analýza tvaru, binární rozhodovací diagramy, druhořádová logika, haldy, jazyková inkluze, konečný automat, monadická logika, nedeterminismus, regulární stromový model checking, separační logika, simulace, stromový automat, formální verifikace
@phdthesis{FITPT519,
author = "Ond\v{r}ej Leng\'{a}l",
type = "Diserta\v{c}n\'{i} pr\'{a}ce",
title = "Automata in Infinite-state 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 = 2015,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/phd-thesis/519/"
}