Verifikace nekonečně stavových systémů založená na konečných automatech
Cíle projektu
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ů.
Klíčová slova
formalverificationinfinitestatesystemspointerprogramsstringmanipulatingprogramssymbolicencodingregularmodelcheckingfiniteautomatalanguageinclusionminimizationsimulationrelation
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Postdoktorandské granty
Veřejná soutěž
Postdoktorandské granty 14 (SGA0201300006)
Hlavní účastníci
—
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
13-37876P
Alternativní jazyk
Název projektu anglicky
Verification of Infinite State Systems Based on Finite Automata
Anotace anglicky
The focus of this project is formal verification of programs with infinite state spaces. Specifically, we target programs with dynamically allocated pointer data structures and programs manipulating unbounded strings. Verification methods for both of these classes are highly desirable. The former are notoriously error-prone, hard to debug and reason about, and the latter form the main body of web applications where errors may easily lead to security vulnerabilities. We will build on methods based on symbolically encoding sets of program states using finite automata, such as regular model checking. In a connection to that, we will also investigate theory and methods facilitating practical use of finite automata in general. This especially concerns language inclusion and equivalence testing, size reduction and minimization, and decision procedures for the logics WSkS and MSO. The work on the project will include rigorous mathematical description of the developed principles and algorithms as well as their implementation and experimental evaluation.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
CEP - hlavní obor
IN - Informatika
CEP - vedlejší obor
—
CEP - další vedlejší obor
—
OECD FORD - odpovídající obory
(dle převodníku)10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Hodnocení dokončeného projektu
Hodnocení poskytovatelem
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Zhodnocení výsledků projektu
V rámci mezinárodní i národní spolupráce projekt posunul stav poznání v oblasti verifikace systémů, s výsledky prezentovanými na špičkových světových fórech (mj. na konferencích CAV a TACAS ). Součástí projektu byl i vývoj softwarových nástrojů pro veri?
Termíny řešení
Zahájení řešení
1. 2. 2013
Ukončení řešení
31. 12. 2015
Poslední stav řešení
U - Ukončený projekt
Poslední uvolnění podpory
10. 4. 2015
Dodání dat do CEP
Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP16-GA0-GP-U/01:1
Datum dodání záznamu
6. 5. 2016
Finance
Celkové uznané náklady
2 289 tis. Kč
Výše podpory ze státního rozpočtu
2 289 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Uznané náklady
2 289 tis. Kč
Statní podpora
2 289 tis. Kč
0%
Poskytovatel
Grantová agentura České republiky
CEP
IN - Informatika
Doba řešení
01. 02. 2013 - 31. 12. 2015