Vše
Vše

Co hledáte?

Vše
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

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č

Základní informace

Uznané náklady

2 289 tis. Kč

Statní podpora

2 289 tis. Kč

100%


Poskytovatel

Grantová agentura České republiky

CEP

IN - Informatika

Doba řešení

01. 02. 2013 - 31. 12. 2015