Project - Efektivní konečné automaty pro automatické usuzování

Funding resources

Ministerstvo školství, mládeže a tělovýchovy ČR - ERC CZ

- whole funder (2020-01-01 - 2024-12-31)

On the project

Cílem projektu je zlepšit efektivitu základních technik konečných automatů. Konečný automat je základní koncepcí informatiky s četnými aplikacemi. Výzkum automatů přináší neustále nové výsledky týkající se široké škály aplikací v automatizovaném rozhodování, formálním ověřování, zpracování jazyka, databázích a webových technologiích. Bohužel jejich praktický dopad, i když je pozoruhodný, je do značné míry omezen nedostatečnou škálovatelností automatických technik zakořeněné ve velmi základních pojmech a algoritmech. Efektivnost automatické technologie však není dostatečně vyřešena. Výzkum se většinou zaměřuje na různá rozšíření automatů a vzrušující "teoretické" aplikace. Důvodem této nedostatečné pozornosti je skutečnost, že se základní automatizační techniky zdají být z obvyklé automatické teoretické perspektivy již dobře pochopené, a proto neposkytují dostatek prostoru pro výzkum. Je zapotřebí vyvinout soustředěné úsilí a přijít s novými myšlenkami v mnohem pragmatickějším směru, abych mohlo dojít k posunutí vývoje. Příležitost v dosažení průlomu v efektivnosti rozhodování vidím ve využití automatů, které vychází z pokroku v automatizovaném rozhodování a ověřování. Koncepty, jako je líné hodnocení, symbolické reprezentace, abstrakce nebo heuristika z řešení SAT / SMT, lze kombinovat s tradičními automatovými technikami a zpracovat novým způsobem. Plánuji detailně prozkoumat základní automatové nástroje společně s těmito koncepty s důrazem na jejich výkonnost v praxi. Jsem přesvědčen, že když výkonnost v praxi získává zaslouženou pozornost, můžeme očekávat podobně rychlý pokrok, jaký byl např. u řešení problému SAT / SMT nebo u ověřování softwaru, což může vést k velmi užitečným a prakticky škálovatelným metodám a nástrojům, stejně jako k novým příležitostem pro hluboké teoretické studium nových technik.

Description in English
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.

Keywords
konečné automaty, logika, automatizované uvažování, formální verifikace, analýza programu, analýza tvaru, analýza řetězcových programů, bezpečnost

Key words in English
finite automata, logic, automated reasoning, formal verification, program analysis, shape analysis, string program analysis, security

Mark

LL1908

Default language

Czech

People responsible

Units

Department of Intelligent Systems
- beneficiary (2019-07-16 - 2024-12-31)

Results

KŘIVKA, Z.; MEDUNA, A. Scattered Context Grammars with One Non-Context-Free Production are Computationally Complete. Fundamenta Informaticae, 2021, vol. 179, no. 4, p. 361-384. ISSN: 0169-2968.
Detail

JOBRANOVÁ, S.; LENGÁL, O.; CHEN, T.; CHEN, Y.; JIANG, J. Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization. IEEE/ACM International Conference on Computer-Aided Design (ICCAD '24), October 27--31, 2024, New York, NY, USA. Association for Computing Machinery, 2024. p. 0-0. ISBN: 979-8-4007-1077-3.
Detail

HAVLENA, V.; LENGÁL, O.; CHEN, Y.; TURRINI, A. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In Proceedings of APLAS'20. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2020. p. 343-363. ISSN: 0302-9743.
Detail

MATOUŠEK, P.; HAVLENA, V.; HOLÍK, L. 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. p. 81-89. ISBN: 978-3-903176-32-4.
Detail

HOLÍKOVÁ, L.; HOLÍK, L.; LENGÁL, O.; SAARIKIVI, O.; VEANES, M.; VOJNAR, T. Regex Matching with Counting-Set Automata. Proceedings of the ACM on Programming Languages, 2020, vol. 4, no. 11, p. 1-30. ISSN: 2475-1421.
Detail

HOLÍK, L.; JANKŮ, P.; BUI PHI, D.; CHEN, Y.; LIN, H.; WU, W.; ABDULLA, P.; ATIG, M. 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. p. 943-957. ISBN: 978-1-4503-7613-6.
Detail

SÍČ, J.; STREJČEK, J. DQBDD: An Efficient BDD-Based DQBF Solver. In Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2021. p. 535-544. ISSN: 0302-9743.
Detail

HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VALEŠ, O.; VOJNAR, T. Antiprenexing for WSkS: A Little Goes a Long Way. In EPiC Series in Computing. Proceedings of LPAR-23. Manchester: EasyChair, 2020. p. 298-316. ISSN: 2398-7340.
Detail

HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O.; HABERMEHL, P. Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. Proceedings of CAV'24. Lecture Notes in Computer Science. Montreal: Springer Verlag, 2024. p. 42-67. ISSN: 0302-9743.
Detail

HOLÍK, L.; ŠEDÝ, M. Utilization of Repeating Substructures for Efficient Representation of Automata (Technical Report). Brno: 2023. p. 1-12.
Detail

DACÍK, T.; ROGALEWICZ, A.; VOJNAR, T.; ZULEGER, F. Deciding Boolean Separation Logic via Small Models. 2024. p. 0-0.
Detail

CHEN, Y.; CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J. Solving String Constraints with Lengths by Stabilization. Proceedings of the ACM on Programming Languages, 2023, vol. 7, no. 10, p. 2112-2141. ISSN: 2475-1421.
Detail

HOLÍKOVÁ, L.; HOLÍK, L.; HOMOLIAK, I.; LENGÁL, O.; VEANES, M.; VOJNAR, T. Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. In Proceedings of the 31st USENIX Security Symposium. Boston, MA: USENIX, 2022. p. 4165-4182. ISBN: 978-1-939133-31-1.
Detail

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementing Büchi Automata with Ranker. In Proceedings of the 34th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Haifa: Springer Verlag, 2022. p. 188-201. ISBN: 978-3-031-13187-5. ISSN: 0302-9743.
Detail

HOLÍK, L.; PERINGER, P.; ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; ZULEGER, F. Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics, LIPIcs. Leibniz International Proceedings in Informatics. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2022. p. 1-30. ISBN: 978-3-95977-225-9. ISSN: 1868-8969.
Detail

ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; HOLÍK, L.; PERINGER, P.; ZULEGER, F. Low-Level Bi-Abduction (Artifact). Dagstuhl: 2022. p. 1-6.
Detail

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementing Büchi Automata with Ranker (Technical Report). Ithaca: Cornell University Library, 2022. p. 0-0.
Detail

HOLÍK, L.; PERINGER, P.; ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; ZULEGER, F. Low-Level Bi-Abduction (technical report). Ithaca: 2022. p. 0-0.
Detail

HAMMER, J.; KŘIVKA, Z. Practical Aspects of Membership Problem of Watson-Crick Context-free Grammars. In Proceedings 12th International Workshop on Non-Classical Models of Automata and Applications. Electronic Proceedings in Theoretical Computer Science, EPTCS. Debrecen: School of Computer Science and Engineering, University of New South Wales, 2022. p. 88-111. ISSN: 2075-2180.
Detail

KLOBUČNÍKOVÁ, D.; KŘIVKA, Z.; MEDUNA, A. Conclusive Tree-Controlled Grammars. In Proceedings 12th International Workshop on Non-Classical Models of Automata and Applications. Electronic Proceedings in Theoretical Computer Science, EPTCS. Debrecen: School of Computer Science and Engineering, University of New South Wales, 2022. p. 112-125. ISSN: 2075-2180.
Detail

SÍČ, J.; GE-ERNST, A.; SCHOLL, C.; WIMMER, R. Solving dependency quantified Boolean formulas using quantifier localization. Theoretical Computer Science, 2022, vol. 2022, no. 925, p. 1-24. ISSN: 0304-3975.
Detail

HOLÍK, L.; HOLÍKOVÁ, L.; SÍČ, J.; VOJNAR, T. Fast Matching of Regular Patterns with Synchronizing Counting (Technical Report). Ithaca: 2023. p. 1-32.
Detail

HAVLENA, V.; ŠMAHLÍKOVÁ, B.; LENGÁL, O.; LI, Y.; TURRINI, A. Modular Mix-and-Match Complementation of Büchi Automata. In Proceedings of TACAS'23. Lecture Notes in Computer Science. Paris: Springer Verlag, 2023. p. 249-270. ISSN: 0302-9743.
Detail

HAVLENA, V.; ŠMAHLÍKOVÁ, B.; LENGÁL, O.; LI, Y.; TURRINI, A. Modular Mix-and-Match Complementation of Büchi Automata (Technical Report). Ithaca: Cornell University Library, 2023. p. 1-37.
Detail

HOLÍK, L.; ABDULLA, P.; ATIG, M.; BUI PHI, D.; CHEN, Y.; WU, Z. 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. p. 305-320. ISBN: 978-3-030-89051-3.
Detail

HAVLENA, V.; LENGÁL, O.; CHEN, Y.; TURRINI, A. A symbolic algorithm for the case-split rule in solving word constraints with extensions. JOURNAL OF SYSTEMS AND SOFTWARE, 2023, vol. 201, no. 201, p. 111673-111693. ISSN: 0164-1212.
Detail

HAVLENA, V.; CHOCHOLATÝ, D.; LENGÁL, O.; HOLÍK, L.; SÍČ, J.; BLAHOUDEK, F.; CHEN, Y. Word Equations in Synergy with Regular Constraints. In Proceedings of FM'23. Lecture Notes in Computer Science. Lübeck: Springer Verlag, 2023. p. 403-423. ISSN: 0302-9743.
Detail

HOLÍK, L.; HOLÍKOVÁ, L.; SÍČ, J.; VOJNAR, T. Fast Matching of Regular Patterns with Synchronizing Counting. In Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2023. p. 392-412. ISSN: 0302-9743.
Detail

LENGÁL, O.; CHEN, Y.; TSAI, W.; LIN, J.; CHUNG, K.; YEN, D. An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. Proceedings of the ACM on Programming Languages, 2023, vol. 7, no. 6, p. 1218-1243. ISSN: 2475-1421.
Detail

LENGÁL, O.; CHEN, Y.; TSAI, W.; CHUNG, K.; LIN, J. AutoQ: An Automata-based Quantum Circuit Verifier. In Proceedings of 35th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer Verlag, 2023. p. 139-153. ISSN: 0302-9743.
Detail

HOLÍK, L.; HRUŠKA, M.; SÍČ, J.; VARGOVČÍK, P.; FIEDOR, T.; ROGALEWICZ, A. Reasoning about Regular Properties: A Comparative Study. In Automated Deduction - CADE 29. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2023. p. 286-306. ISSN: 0302-9743.
Detail

ANDRIUSHCHENKO, R.; BARTOCCI, E.; ČEŠKA, M.; FRANCESCO, P.; SARAH, S. 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). Cham: Springer Verlag, 2023. p. 288-306. ISBN: 978-3-031-43834-9.
Detail

HAVLENA, V.; HOLÍK, L.; CHOCHOLATÝ, D.; LENGÁL, O.; SÍČ, J.; CHEN, Y.: Z3-Noodler; Z3-Noodler: A String Solver. https://github.com/VeriFIT/z3-noodler. URL: https://github.com/VeriFIT/z3-noodler. (software)
Detail

HAVLENA, V.; HOLÍK, L.; CHOCHOLATÝ, D.; LENGÁL, O.; SÍČ, J.; FIEDOR, T.; HRUŠKA, M.: mata; Mata: A Finite Automata Library. https://github.com/VeriFIT/mata. URL: https://github.com/VeriFIT/mata. (software)
Detail

HOLÍK, L.; HOLÍKOVÁ, L.; HOMOLIAK, I.; LENGÁL, O.; VOJNAR, T.; VEANES, M.: gadgetca; GadgetCA: A Tool for Generating ReDoS Attacks. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/gadgetca. URL: https://www.fit.vut.cz/research/product/730/. (software)
Detail

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B.: Ranker; Ranker: A Tool for Complementing Büchi Automata. https://github.com/vhavlena/ranker. URL: https://github.com/vhavlena/ranker. (software)
Detail

ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; HOLÍK, L.; PERINGER, P.; ZULEGER, F.: broom; Broom: A Static Analyzer for C Based on Separation Logic and the Principle of Bi-Abductive Reasoning. https://pajda.fit.vutbr.cz/rogalew/broom/-/tree/v0.0.1. URL: https://pajda.fit.vutbr.cz/rogalew/broom/-/tree/v0.0.1. (software)
Detail

Responsibility: Holík Lukáš, doc. Mgr., Ph.D.

VUT

Faculties

University Institutes

Parts

Efficient Finite Automata for Automated Reasoning