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áš, doc. Mgr., Ph.D. (DITS FIT BUT) , research leader
Blahoudek František, RNDr., Ph.D. (DITS FIT BUT)
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT)
Fiedor Tomáš, Ing., Ph.D. (DITS FIT BUT)
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Holíková Lenka, Ing. (DITS FIT BUT)
Homoliak Ivan, doc. Ing., Ph.D. (DITS FIT BUT)
Horký Michal, Ing. (FIT BUT)
Hošták Viliam Samuel, Ing. (FIT BUT)
Hruška Martin, Ing. (DITS FIT BUT)
Jawed Soyiba, Ph.D. (DCSY FIT BUT)
Kesiraju Michaela, Bc. (FIT BUT)
Křivka Zbyněk, Ing., Ph.D. (DIFS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Macák Filip, Ing. (DITS FIT BUT)
Martiček Štefan, Ing. (DITS FIT BUT)
Meduna Alexander, prof. RNDr., CSc. (DIFS FIT BUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Síč Juraj, Mgr. (DITS FIT BUT)
Slezáková Alexandra, Bc. (FIT BUT)
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT)
Šedý Michal, Ing. (FIT BUT)
Šoková Veronika, Ing. (DITS FIT BUT)
Toth Vaňo Pavol, Ing. (FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Publications

2025

  • ABDULLA Parosh A., CHEN Yo-ga, CHEN Yu-Fang, HOLÍK Lukáš, LENGÁL Ondřej, LIN Jyun-ao, LO Fang-yi and TSAI Wei-lun. Verifying Quantum Circuits with Level-Synchronized Tree Automata. Proceedings of the ACM on Programming Languages, vol. 9, no. 1, 2025, p. 31. ISSN 2475-1421. Detail

2024

  • CHEN Tian-fu, CHEN Yu-Fang, JIANG Jie-hong, JOBRANOVÁ Sára and LENGÁL Ondřej. Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization. In: IEEE/ACM International Conference on Computer-Aided Design (ICCAD '24), October 27--31, 2024, New York, NY, USA. Association for Computing Machinery, 2024. ISBN 979-8-4007-1077-3. Detail
  • HABERMEHL Peter, HAVLENA Vojtěch, HEČKO Michal, HOLÍK Lukáš and LENGÁL Ondřej. Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. In: Proceedings of CAV'24. Montreal: Springer Verlag, 2024, pp. 42-67. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and SÍČ Juraj. Cooking String-Integer Conversions with Noodles. In: Proceedings of SAT'24. Leibniz International Proceedings in Informatics (LIPIcs). Pune: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2024, pp. 1-19. ISSN 1868-8969. Detail
  • DACÍK Tomáš, ROGALEWICZ Adam, VOJNAR Tomáš and ZULEGER Florian. Deciding Boolean Separation Logic via Small Models. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 14570. Cham: Springer Nature Switzerland AG, 2024, pp. 188-206. ISBN 978-3-031-57245-6. Detail
  • FIEDOR Tomáš, HAVLENA Vojtěch, HOLÍK Lukáš, HRUŠKA Martin, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Mata: A Fast and Simple Finite Automata Library. In: Proceedings of TACAS'24. Luxembourgh: Springer Verlag, 2024, pp. 130-151. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, HOLÍK Lukáš, CHEN Yu-Fang, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Z3-Noodler: An Automata-based String Solver. In: Proceedings of TACAS'24. Lecture Notes. Luxembourgh: Springer Verlag, 2024, pp. 24-33. ISSN 0302-9743. Detail

2023

  • HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej and TURRINI Andrea. A symbolic algorithm for the case-split rule in solving word constraints with extensions. Journal of Systems and Software, vol. 201, no. 201, 2023, pp. 111673-111693. ISSN 0164-1212. Detail
  • CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao, TSAI Wei-lun and YEN Di-de. An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. Proceedings of the ACM on Programming Languages, vol. 7, no. 6, 2023, pp. 1218-1243. ISSN 2475-1421. Detail
  • CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao and TSAI Wei-lun. AutoQ: An Automata-based Quantum Circuit Verifier. In: Proceedings of 35th International Conference on Computer Aided Verification. Cham: Springer Verlag, 2023, pp. 139-153. ISSN 0302-9743. Detail
  • ANDRIUSHCHENKO Roman, BARTOCCI Ezio, ČEŠKA Milan, FRANCESCO Pontiggia and SARAH Sallinger. Deductive Controller Synthesis for Probabilistic Hyperproperties. In: Quantitative Evaluation of SysTems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14287. Cham: Springer Verlag, 2023, pp. 288-306. ISBN 978-3-031-43834-9. Detail
  • HOLÍK Lukáš, HOLÍKOVÁ Lenka, SÍČ Juraj and VOJNAR Tomáš. Fast Matching of Regular Patterns with Synchronizing Counting. In: Foundations of Software Science and Computation Structures. Heidelberg: Springer Verlag, 2023, pp. 392-412. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, HOLÍKOVÁ Lenka, SÍČ Juraj and VOJNAR Tomáš. Fast Matching of Regular Patterns with Synchronizing Counting (Technical Report). Ithaca, 2023. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej, LI Yong, ŠMAHLÍKOVÁ Barbora and TURRINI Andrea. Modular Mix-and-Match Complementation of Büchi Automata. In: Proceedings of TACAS'23. Paris: Springer Verlag, 2023, pp. 249-270. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej, LI Yong, ŠMAHLÍKOVÁ Barbora and TURRINI Andrea. Modular Mix-and-Match Complementation of Büchi Automata (Technical Report). Ithaca: Cornell University Library, 2023. Detail
  • FIEDOR Tomáš, HOLÍK Lukáš, HRUŠKA Martin, ROGALEWICZ Adam, SÍČ Juraj and VARGOVČÍK Pavol. Reasoning about Regular Properties: A Comparative Study. In: Automated Deduction - CADE 29. Cham: Springer Nature Switzerland AG, 2023, pp. 286-306. ISSN 0302-9743. Detail
  • CHEN Yu-Fang, CHOCHOLATÝ David, HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and SÍČ Juraj. Solving String Constraints with Lengths by Stabilization. Proceedings of the ACM on Programming Languages, vol. 7, no. 10, 2023, pp. 2112-2141. ISSN 2475-1421. Detail
  • HOLÍK Lukáš and ŠEDÝ Michal. Utilization of Repeating Substructures for Efficient Representation of Automata (Technical Report). Brno, 2023. Detail
  • BLAHOUDEK František, HAVLENA Vojtěch, HOLÍK Lukáš, CHEN Yu-Fang, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Word Equations in Synergy with Regular Constraints. In: Proceedings of FM'23. Lübeck: Springer Verlag, 2023, pp. 403-423. ISSN 0302-9743. Detail

2022

  • HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Complementing Büchi Automata with Ranker. In: Proceedings of the 34th International Conference on Computer Aided Verification. Haifa: Springer Verlag, 2022, pp. 188-201. ISBN 978-3-031-13187-5. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Complementing Büchi Automata with Ranker (Technical Report). Ithaca: Cornell University Library, 2022. Detail
  • KLOBUČNÍKOVÁ Dominika, KŘIVKA Zbyněk and MEDUNA Alexander. Conclusive Tree-Controlled Grammars. In: Proceedings 12th International Workshop on Non-Classical Models of Automata and Applications . Debrecen: School of Computer Science and Engineering, University of New South Wales, 2022, pp. 112-125. ISSN 2075-2180. Detail
  • HOLÍKOVÁ Lenka, HOLÍK Lukáš, HOMOLIAK Ivan, LENGÁL Ondřej, VEANES Margus and VOJNAR Tomáš. Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. In: Proceedings of the 31st USENIX Security Symposium. Boston, MA: USENIX, 2022, pp. 4165-4182. ISBN 978-1-939133-31-1. Detail
  • HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš and ZULEGER Florian. Low-Level Bi-Abduction. In: 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics, vol. 2022. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2022, pp. 1-30. ISBN 978-3-95977-225-9. ISSN 1868-8969. Detail
  • HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš and ZULEGER Florian. Low-Level Bi-Abduction (Artifact). Dagstuhl, 2022. Detail
  • HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš and ZULEGER Florian. Low-Level Bi-Abduction (technical report). Ithaca, 2022. Detail
  • HAMMER Jan and KŘIVKA Zbyněk. Practical Aspects of Membership Problem of Watson-Crick Context-free Grammars. In: Proceedings 12th International Workshop on Non-Classical Models of Automata and Applications . Debrecen: School of Computer Science and Engineering, University of New South Wales, 2022, pp. 88-111. ISSN 2075-2180. Detail
  • GE-ERNST Aile, SCHOLL Christoph, SÍČ Juraj and WIMMER Ralf. Solving dependency quantified Boolean formulas using quantifier localization. Theoretical Computer Science, vol. 2022, no. 925, pp. 1-24. ISSN 0304-3975. Detail

2021

  • SÍČ Juraj and STREJČEK Jan. DQBDD: An Efficient BDD-Based DQBF Solver. In: Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing. Heidelberg: Springer Verlag, 2021, pp. 535-544. ISSN 0302-9743. Detail
  • MATOUŠEK Petr, HAVLENA Vojtěch and HOLÍK Lukáš. Efficient Modelling of ICS Communication For Anomaly Detection Using Probabilistic Automata. In: Proceedings of IFIP/IEEE International Symposium on Integrated Network Management. Bordeaux: International Federation for Information Processing, 2021, pp. 81-89. ISBN 978-3-903176-32-4. Detail
  • KŘIVKA Zbyněk and MEDUNA Alexander. Scattered Context Grammars with One Non-Context-Free Production are Computationally Complete. Fundamenta Informaticae, vol. 179, no. 4, 2021, pp. 361-384. ISSN 0169-2968. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang and WU Zhilin. Solving Not-Substring Constraint with Flat Abstraction. In: Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings. 13008. Berlín: Springer International Publishing, 2021, pp. 305-320. ISBN 978-3-030-89051-3. Detail

2020

  • HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej and TURRINI Andrea. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In: Proceedings of APLAS'20. Heidelberg: Springer Verlag, 2020, pp. 343-363. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej, VALEŠ Ondřej and VOJNAR Tomáš. Antiprenexing for WSkS: A Little Goes a Long Way. In: EPiC Series in Computing. Proceedings of LPAR-23. Manchester: EasyChair, 2020, pp. 298-316. ISSN 2398-7340. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang, JANKŮ Petr, LIN Hsin-Hung and WU Wei-Cheng. Efficient handling of string-number conversion. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). New York: Association for Computing Machinery, 2020, pp. 943-957. ISBN 978-1-4503-7613-6. Detail
  • HOLÍKOVÁ Lenka, HOLÍK Lukáš, LENGÁL Ondřej, SAARIKIVI Olli, VEANES Margus and VOJNAR Tomáš. Regex Matching with Counting-Set Automata. Proceedings of the ACM on Programming Languages, vol. 4, no. 11, 2020, pp. 1-30. ISSN 2475-1421. Detail
Products

2024

  • Mata: A Finite Automata Library, software, 2024
    Authors: Fiedor Tomáš, Havlena Vojtěch, Holík Lukáš, Hruška Martin, Chocholatý David, Lengál Ondřej, Síč Juraj Detail
  • Z3-Noodler: A String Solver, software, 2024
    Authors: Havlena Vojtěch, Holík Lukáš, Chen Yu-Fang, Chocholatý David, Lengál Ondřej, Síč Juraj Detail

2022

  • Broom: A Static Analyzer for C Based on Separation Logic and the Principle of Bi-Abductive Reasoning, software, 2022
    Authors: Holík Lukáš, Peringer Petr, Rogalewicz Adam, Šoková Veronika, Vojnar Tomáš, Zuleger Florian Detail
  • GadgetCA: A Tool for Generating ReDoS Attacks, software, 2022
    Authors: Holík Lukáš, Holíková Lenka, Homoliak Ivan, Lengál Ondřej, Veanes Margus, Vojnar Tomáš Detail
  • Ranker: A Tool for Complementing Büchi Automata, software, 2022
    Authors: Havlena Vojtěch, Lengál Ondřej, Šmahlíková Barbora Detail
Back to top