Detail projektu

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

Období řešení: 1. 1. 2020 – 31. 12. 2024

Typ projektu: grant

Kód: LL1908

Agentura: Ministerstvo školství, mládeže a tělovýchovy ČR

Program: ERC CZ

Název anglicky
Efficient Finite Automata for Automated Reasoning
Typ
grant
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

Abstrakt

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.

Řešitelé
Holík Lukáš, doc. Mgr., Ph.D. (UITS) – hlavní řešitel
Blahoudek František, RNDr., Ph.D.
Češka Milan, doc. RNDr., Ph.D. (UITS)
Fiedor Tomáš, Ing., Ph.D. (VZ VERIFIT)
Havlena Vojtěch, Ing., Ph.D. (UITS)
Holíková Lenka, Ing., Ph.D. (VZ VERIFIT)
Homoliak Ivan, doc. Ing., Ph.D. (UITS)
Horký Michal, Ing.
Hošták Viliam Samuel, Ing.
Hruška Martin, Ing., Ph.D. (VZ Automata@FIT)
Jawed Soyiba, Dr., MSc (VZ Automata@FIT)
Kesiraju Michaela, Bc.
Křivka Zbyněk, Ing., Ph.D. (UIFS)
Lengál Ondřej, Ing., Ph.D. (UITS)
Macák Filip, Ing. (UITS)
Martiček Štefan, Ing.
Meduna Alexandr, prof. RNDr., CSc. (UIFS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Síč Juraj, Mgr. (UITS)
Slezáková Alexandra, Bc.
Smrčka Aleš, Ing., Ph.D. (UITS)
Šedý Michal, Ing. (UITS)
Šoková Veronika, Ing. (VZ VERIFIT)
Toth Vaňo Pavol, Ing.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Publikace

2025

  • ABDULLA, P.; CHEN, Y.; CHEN, Y.; HOLÍK, L.; LENGÁL, O.; LIN, J.; LO, F.; TSAI, W. Verifying Quantum Circuits with Level-Synchronized Tree Automata. Proceedings of the ACM on Programming Languages, 2025, vol. 9, no. 1, p. 923-953. ISSN: 2475-1421. Detail
  • HAVLENA, V.; CHOCHOLATÝ, D.; LENGÁL, O.; HOLÍK, L.; SÍČ, J.; BLAHOUDEK, F.; CHEN, Y. Word equations in synergy with regular constraints (extended version). Constraints, 2025. ISSN: 1572-9354. Detail
  • JOBRANOVÁ, S.; LENGÁL, O.; CHEN, Y.; CHEN, T.; 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. New York: Association for Computing Machinery, 2025. p. 1-9. ISBN: 979-8-4007-1077-3. Detail
  • LENGÁL, O.; CHEN, Y.; LIN, J.; TSAI, W.; HSIEH, M.; HUANG, W.; CHUNG, K. AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs. In Proceedings of TACAS'25. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2025. p. 87-108. ISSN: 0302-9743. Detail
  • ŠMAHLÍKOVÁ, B.; HAVLENA, V.; LENGÁL, O. Complementation of Emerson-Lei Automata. Proceedings of FoSSaCS'25. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2025. p. 88-110. ISSN: 0302-9743. Detail

2024

  • DACÍK, T.; ROGALEWICZ, A.; VOJNAR, T.; ZULEGER, F. Deciding Boolean Separation Logic via Small Models. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2024. p. 188-206. ISBN: 978-3-031-57245-6. 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
  • HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J. Cooking String-Integer Conversions with Noodles. Proceedings of SAT'24. Leibniz International Proceedings in Informatics, LIPIcs. Leibniz International Proceedings in Informatics (LIPIcs). Pune: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2024. p. 1-19. ISSN: 1868-8969. Detail
  • HOLÍK, L.; CHOCHOLATÝ, D.; FIEDOR, T.; HAVLENA, V.; HRUŠKA, M.; LENGÁL, O.; SÍČ, J. Mata: A Fast and Simple Finite Automata Library. Proceedings of TACAS'24. Lecture Notes in Computer Science. Luxembourgh: Springer Verlag, 2024. p. 130-151. ISSN: 0302-9743. Detail
  • CHEN, Y.; CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J. Z3-Noodler: An Automata-based String Solver. Proceedings of TACAS'24. Lecture Notes in Computer Science. Lecture Notes. Luxembourgh: Springer Verlag, 2024. p. 24-33. ISSN: 0302-9743. Detail
  • VARGOVČÍK, P.; HOLÍK, L. Antichain with SAT and Tries. 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics, LIPIcs. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2024. p. 1-15. ISBN: 978-3-95977-334-8. ISSN: 1868-8969. Detail

2023

  • 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.; 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
  • 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.; Š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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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

2022

  • 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
  • HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementing Büchi Automata with Ranker (Technical Report). Ithaca: Cornell University Library, 2022. 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 (technical report). Ithaca: 2022. 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
  • 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
  • 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
  • ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; HOLÍK, L.; PERINGER, P.; ZULEGER, F. Low-Level Bi-Abduction (Artifact). Dagstuhl: 2022. p. 1-6. 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

2021

  • 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
  • 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
  • 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
  • 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

2020

  • 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.; 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
  • 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
  • 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
Produkty

2024

2022

Nahoru