Project Details

Efektivní konečné automaty pro automatické usuzování

Project Period: 1. 1. 2020 - 31. 12. 2024

Project Type: grant

Code: LL1908

Agency: Ministry of Education, Youth and Sports Czech Republic

Program: ERC CZ

English title
Efficient Finite Automata for Automated Reasoning
Type
grant
Keywords

finite automata, logic, automated reasoning, formal verification, program analysis, shape analysis, string program analysis, security

Abstract


The project aims at improving the efficiency of basic techniques of finite automata technology. Finite automaton is a core concept of computer science, with numerous practical applications, with compilers and pattern matching among the most established ones, and with a vast and continuously expanding space of theoretical possibilities on the verge of being practically applicable, in automated reasoning, formal verification, modelling, language processing, databases, web technologies, and many other areas. The practical impact of automata theory is however limited by insufficient scalability of automata technology, and research in practical efficiency of basic automata technology is not being addressed sufficiently. The basic automata techniques seem well understood and do not yield research opportunities easily, and so most of automata related research focuses on various more complex automata extensions and their exciting possibilities, even though still inheriting all the scalability problems of the basic model.
The main thesis of this project is that (1) the practical scalability of basic automata technology needs to be addressed more in order to unlock the theoretical potential of basic automata as well as of their extensions,
and that (2) it is indeed possible to do that. 
To this end, we will put the basic automata toolkit under a detailed scrutiny with a strong focus on practical performance, and utilise advances in modern automated reasoning and verification. Concepts such as lazy evaluation, alternation, symbolic representation, abstraction, or heuristics from SAT/SMT solving can be combined with traditional automata techniques and elaborated on in novel ways. To maintain a connection to practice, we will drive our research by a research in application domains of automata. We will namely focus on string constraint solving (e.g., for vulnerability analysis of string manipulating programs), pattern matching (e.g., classical pattern matching, hardware accelerated pattern matching in network monitoring), shape analysis (low level pointer program analysis, analysis of programs with complex data structures, of parallel pointer programs), automata learning (e.g., learning of network traffic characteristics for fast anomaly detection).
We believe that a concentrated focus on practical efficiency of automata can initiate a success story similarly to that of SAT/SMT solving, ultimately yielding widely useful and practically scalable methods and tools and also opportunities for a practically relevant theoretical research.

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., Ph.D. (UITS FIT VUT)
Havlena Vojtěch, Ing. (UITS FIT VUT)
Křivka Zbyněk, Ing., Ph.D. (UIFS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Meduna Alexander, prof. RNDr., CSc. (UIFS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Síč Juraj, Bc. (UITS FIT VUT)
Šoková Veronika, Ing. (UITS FIT VUT)
Turoňová Lenka, Ing. (UITS FIT VUT)
Publications

2020

Back to top