Detail projektu

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

Období řešení: 01.01.2020 — 31.12.2024

O projektu

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.

Popis anglicky
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.

Klíčová slova
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

Klíčová slova anglicky
finite automata, logic, automated reasoning, formal verification, program analysis, shape analysis, string program analysis, security

Označení

LL1908

Originální jazyk

čeština

Řešitelé

Útvary

Ústav inteligentních systémů
- příjemce (16.07.2019 - 31.12.2024)

Zdroje financování

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

- plně financující (2020-01-01 - 2024-12-31)

Výsledky

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

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

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

TUROŇOVÁ, 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

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

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

TUROŇOVÁ, 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

HOLÍK, L.; HOMOLIAK, I.; LENGÁL, O.; TUROŇOVÁ, L.; 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