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