Automata@FIT

Information

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.

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

Awards

  • Nomination for the Best paper of ETAPS'24, for the work  Z3-Noodler: An Automata-based String Solver by Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síč
  • Best paper at FM'23 for the work Word Equations in Synergy with Regular Constraints by Frantisek Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
  • Distinguished paper at OOPSLA'23 for the work Solving String Constraints with Lengths by Stabilization by Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Juraj Síč
  • Distinguished paper at PLDI'23 for the work An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits by Yu-Fang Chen, Kai-Min Chung, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen
  • Barbora Šmahlíková won the VCLA International Student Awards 2023 and the Government of the Czech Republic Gifted Student Award for her research

Contact

Lukáš Holík, holik@fit.vutbr.cz

Back to top