Project Details

Efficient Automata Techniques for Formal Reasoning

Project Period: 1. 1. 2016 - 31. 12. 2018

Project Type: grant

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áš, doc. Mgr., Ph.D. (UITS FIT VUT) , research leader
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Publications

2020

2019

2018

2017

2016

Products

2018

2017

Back to top