Research

Automata@FIT is a research group at FIT BUT, founded in 2023, focusing on research around finite automata and related formalisms, their theory, the fundamental principles needed to use them efficiently in applications, and the applications themselves: in formal automatic reasoning, system analysis and verification, deciding logics, SMT-solving, string constraint solving, analysis of quantum circuits, in regular pattern recognition, network monitoring and anomaly detection, formalisms and methods to deal with uncertainty and to support automated decision making.

Main research areas

• Automata and graph theory and formal logics
  • Algorithms for an efficient handling of finite automata, and automata models. Recognizing and learning regular patterns. Deciding logics such as Presburger arithmethic, WSkS, or languages of string constraints.
• String constraints
  • SMT string solving. Analysis of string manipulating programs with applications in analysing security of web applications such as SQL-injection or cross-site scripting, cloud access policies, or model-based test generation.
• Static analysis and verification
  • On formal foundation utilizing automata theory, logics, and graph theory to analyse string manipulating programs, systems with infinite memory, symbolic execution and concolic testing, or model-based test generation.

Current Research

We currently focus on

• development of string constraint solving technology, based on finite automata, with applications in the analysis of string manipulation systems, web application vulnerabilities, security policy analysis, e.g. cloud technologies,
• analysis of quantum circuits using techniques based on tree automata
• automatic procedures for decision logics such as integer linear arithmetic, WS1S, MSO, HyperLTL
• development of general-purpose techniques and tools for efficient use of finite automata
• development of concise extensions to finite automata and decision diagrams and methods for working with them (e.g., alternations, registers, counters, procedures)
• Markov models as a formalism for dealing with uncertainty and supporting automated decision making
• automata in network traffic monitoring and anomaly detection
• efficient regular pattern matching