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

2024

  • DACÍK Tomáš, ROGALEWICZ Adam, VOJNAR Tomáš and ZULEGER Florian. Deciding Boolean Separation Logic via Small Models. In: 2024. 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