Verifikace nekonečně stavových systémů založená na konečných automatech

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

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.

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 <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

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?

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

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

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č