Detail projektu

Verification of Infinite State Systems Based on Finite Automata

Období řešení: 1.2.2013 - 31.12.2015

Kód: GP13-37876P

Agentura: Grantová agentura České republiky

Program: Postdoktorandské granty

Název česky
Verifikace nekonečně stavových systémů založená na konečných automatech
Typ
grant
Klíčová slova
formální verifikace
nekonečně stavové systémy
programy s ukazateli
programy manipulující řetězce
symbolická reprezentace
regulární model checking
konečné automaty
jazyková inkluze
minimalizace
relace simulace
Abstrakt
Projekt je zaměřen na formální verifikaci programů s nekonečnými stavovými prostory, zvláště pak na programy s dynamicky alokovanými ukazatelovými strukturami a programy manipulující řetězce neohraničené délky. Verifikační nástroje pro obě třídy programů jsou žádoucí. Programy s ukazateli jsou notoricky náchylné k výskytům těžko odhalitelných chyb, programy s řetězci jsou jádrem webových aplikací, kde chyba snadno vede ke kritickým bezpečnostním rizikům. Projekt staví na metodách využívajících konečné automaty jako prostředek symbolické reprezentace nekonečných množin stavů. V souvislosti s tím budeme také vyvíjet technologii umožňující využití nedeterministických konečných automatů v praxi, zejména algoritmy pro testování jazykové inkluze, minimalizaci, a rozhodovací procedury logik MSO a WSkS. Práce na projektu bude vedena rigorózními matematickými metodami a bude zahrnovat implementaci a experimentální vyhodnocení navržených technik a algoritmů.
Řešitelé
Holík Lukáš, Mgr., Ph.D. (UITS FIT VUT) , hlavní řešitel
Fiedor Tomáš, Ing. (UITS FIT VUT)
Hruška Martin, Ing. (UITS FIT VUT)
Chaloupka Jan, Ing. (UITS FIT VUT)
Janků Petr, Ing. (FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Turoňová Lenka, Ing. (UITS FIT VUT)
Publikace

2017

2016

2015

2014

2013

Produkty

2015

Nahoru