Techniques avancées pour la vérification de systémes a nombre d'états infini

Efektivita současných technik pro model checking nekonečně stavových systémů je
však stále relativně daleko od jejich skutečně praktické aplikovatelnosti a také
třídy systémů a jejich ověřovaných vlastností, na které se tyto techniky dají
uplatnit, jsou omezené. Cílem tohoto projektu je proto přispět k výzkumu metod
model checkingu nekonečně stavových systémů tak, aby byly v co největší míře
odstraněny jejich současná omezení jak v oblasti efektivity, tak v oblasti
obecnosti. S cílem zvýšit efektivitu současných technik symbolického model
checkingu nekonečně stavových systémů budou v projektu konkrétně zkoumány např.
techniky symbolického model checkingu založené na nedeterministických konečných
automatech, jež by měly umožnit vyhnout se determinizaci, která je jedním
z výpočetně nejdražších kroků v rámci současných přístupů. Za tím účelem je
zapotřebí vyvinout všechny potřebné operace (jako např. ověřování prázdnosti,
inkluze, minimalizace, abstrakce apod.) nad různými používanými typy automatů nad
slovy, stromy atd. Pro zvýšení obecnosti současných technik pak projekt zahrne
jak výzkum možností verifikace složitějších systémů (např. programů s neomezenými
dynamickými datovými strukturami založenými na ukazatelích a současně
s neomezenými celočíselnými proměnnými) i výzkum možností ověřování složitějších
vlastností než dosud (včetně např. konečnosti výpočtu či vlastností typu živost).
Při práci na tomto cíli budou zkoumány různá rozšíření současných automatů
a logik (např. kombinace různých tříd automatů a logik popisujících kvalitativní
strukturu systému s různými kvantitativními omezeními) a také algoritmy pro práci
s takto rozšířenými formalismy, zahrnující např. pokročilé rozhodovací procedury
nad logikami, nové metody abstrakce a učení nad automaty apod. Projekt přitom
zahrne jak teoretický výzkum nových metod automatické verifikace nekonečně
stavových systémů tak také prototypovou implementaci navržených technik tak, aby
jejich vlastnosti mohly být ověřeny na vhodných případových studiích systémů
s neomezenými a/nebo dynamickými strukturami, případně s parametry.