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.