Project Details

Verification of Infinite State Systems Based on Finite Automata

Project Period: 1. 2. 2013 - 31. 12. 2015

Project Type: grant

Code: GP13-37876P

Agency: Czech Science Foundation

Program: Postdoktorandské granty

Czech title
Verifikace nekonečně stavových systémů založená na konečných automatech
Type
grant
Keywords
formal verification
infinite state systems
pointer programs
string manipulating programs
symbolic encoding
regular model checking
finite automata
language inclusion
minimization
simulation relation
Abstract
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.
Team members
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT) , research leader
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Publications

2017

2016

2015

2014

2013

Products

2015

Back to top