Detail projektu

Verification of Infinite State Systems Based on Finite Automata

Období řešení: 1. 2. 2013 - 31. 12. 2015

Typ projektu: grant

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áš, doc. Mgr., Ph.D. (UITS FIT VUT) , hlavní řešitel
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Publikace

2017

2016

2015

2014

2013

Produkty

2015

Nahoru