Efficient finite automata for automated reasoning

We will develop techniques for working with finite automata with applications in automatic reasoning, verification and decision procedures for logics.
Although automata an old and fundamental concept of computer science with a huge number of applications, and very well understood at a basic theoretical level, techniques for their use in practice are a very rich and lively field of research.

The field has very strong practical motivation in areas such as verification and testing, regular pattern search, artificial intelligence and automatic inference, decision procedures for logics and SMT-solving, system design and analysis, and automated synthesis.
For example, the most efficient algorithms for regular pattern search are based on automata, but it is still not clear how to generalize these algorithms to backreferences, repetition counters, or so-called look-arounds. Deciding logics over strings, aka string-solving, has applications in verification of programs with strings, especially in security analysis of web applications (susceptibility to SQL-injection, cross-site-scripting attacks), analysis of cloud access policies, or of models of critical systems in avionics. An open problem is the efficient implementation of automatic decision procedures for integer arithmetic and other logics. Regular model-checking is an automatic method applicable to the verification of a wide range of systems with infinite state space, such as programs with dynamic data structures or communication protocols. Automated techniques can be used to automatically synthesize programs such as communication interfaces and drivers.

In these and other areas, there are a number of deep theoretical questions about decidability and problem complexity.
For example, how to model back-reference using finite automata? What is decidable about programs that manipulate strings, such as web applications, or programs with dynamic data structures? At what cost?

Practical questions concern the efficient implementation of existing automata algorithms and theoretical knowledge.
How to avoid state explosion in complex automata manipulations? How to represent them compactly, using techniques of minimization, syntactic extensions, abstraction, approximation?
How to work efficiently with compact representations of automata, such as alternating automata, symbolic automata, automata with counters and registers? What are the theoretical properties of these extensions? How to efficiently implement the developed techniques so that they really work on concrete practical problems?

In addition to Doc. Holík, part of the VeriFIT research group, Dr. Lengál, Doc. Rogalewicz, Doc. Češka, Prof. Vojnar. The group reaches the top international level, with hundreds of publications in the most prestigious forums, dozens of software tools, numerous international awards, and intensive international cooperation with prestigious research institutions (Microsofr research, Redmond; Academia Sinica, Taipei, Uppsala Univerisy, Univeristy of Braunschweig, University of Edinburgh, Univeristy of Kaserslautern, University of Paris, Université Grenoble Alpes, Chinese Academy of Sciences).
We collaborate with industry (Red Hat, Honeywell). Our PhD graduates thus have opportunities to obtain interesting specialized positions in industry or pursue careers in academia.
The group has been successful in obtaining grants, so PhD students can be rewarded financially.