All
All

What are you looking for?

All
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Verification of Infinite State Systems Based on Finite Automata

Project goals

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.

Keywords

formalverificationinfinitestatesystemspointerprogramsstringmanipulatingprogramssymbolicencodingregularmodelcheckingfiniteautomatalanguageinclusionminimizationsimulationrelation

Public support

  • Provider

    Czech Science Foundation

  • Programme

    Post-graduate (doctorate) grants

  • Call for proposals

    Postdoktorandské granty 14 (SGA0201300006)

  • Main participants

  • Contest type

    VS - Public tender

  • Contract ID

    13-37876P

Alternative language

  • Project name in Czech

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

  • Annotation in Czech

    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ů.

Scientific branches

  • R&D category

    ZV - Basic research

  • CEP classification - main branch

    IN - Informatics

  • CEP - secondary branch

  • CEP - another secondary branch

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

Completed project evaluation

  • Provider evaluation

    U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)

  • Project results evaluation

    Within an international cooperation, the project has shifted the state-of-the-art in the area of system verification, with several results presented at the top venues (like, e.g., conferences CAV and TACAS), which has included developing software tools for program verification.

Solution timeline

  • Realization period - beginning

    Feb 1, 2013

  • Realization period - end

    Dec 31, 2015

  • Project status

    U - Finished project

  • Latest support payment

    Apr 10, 2015

Data delivery to CEP

  • Confidentiality

    S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

  • Data delivery code

    CEP16-GA0-GP-U/01:1

  • Data delivery date

    May 6, 2016

Finance

  • Total approved costs

    2,289 thou. CZK

  • Public financial support

    2,289 thou. CZK

  • Other public sources

    0 thou. CZK

  • Non public and foreign sources

    0 thou. CZK

Basic information

Recognised costs

2 289 CZK thou.

Public support

2 289 CZK thou.

100%


Provider

Czech Science Foundation

CEP

IN - Informatics

Solution period

01. 02. 2013 - 31. 12. 2015