Faculty of Information Technology, BUT

Project Details

Efficient Automata Techniques for Formal Reasoning

Project Period: 01.01.2016 - 31.12.2018

Code: GJ16-24707Y

Agency: Czech Science Foundation

Program: Juniorské granty

Czech title
Efektivní automaty pro formální rozhodování
Type
grant
Keywords
finite automata
formal verification
logics
decision procedures
string analysis
shape analysis
parallelism
concurrency
context-free languages
SAT
SMT

Abstract
The project focuses on development of efficient algorithms for finite automata applicable in formal verification and analysis of dynamic systems. The central idea is to explore connections between automata, SAT/SMT solving, and program verification. We believe that because all these three domains solve similar problems, interchanging ideas between the domains is possible and may significantly advance not only the domain of automata but also the other mentioned areas. The automata-based algorithms developed in the project will in particular target the following four lively domains of applications: analysis of string manipulating programs, shape analysis, verification of concurrent programs, and decision procedures of selected logics suitable for verification of infinite-state systems (such as WSkS or separation logic). 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áš, Mgr., Ph.D. (UITS FIT VUT) , research leader
Češka Milan, RNDr., Ph.D. (UITS FIT VUT)
Fiedor Tomáš, Ing. (UITS FIT VUT)
Havlena Vojtěch, Ing. (UITS FIT VUT)
Hruška Martin, Ing. (UITS FIT VUT)
Janků Petr, Ing. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Síč Juraj, Bc. (FIT VUT)
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Šoková Veronika, Ing. (UITS FIT VUT)
Turoňová Lenka, Ing. (UITS FIT VUT)
Publications

2019

2018

2017

2016

Products

2018

2017

Back to top