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
Č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. (UITS)
Křivka Zbyněk, Ing., Ph.D. (UIFS)
Lengál Ondřej, Ing., Ph.D. (UITS)
Meduna Alexandr, prof. RNDr., CSc. (UIFS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Síč Juraj, Mgr. (UITS)
Šoková Veronika, Ing. (UITS)
Publikace

2024

  • DACÍK, T.; ROGALEWICZ, A.; VOJNAR, T.; ZULEGER, F. Deciding Boolean Separation Logic via Small Models. 2024. p. 0-0. 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
  • 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

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 (Technical Report). Ithaca: 2023. p. 1-32. 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
  • HOLÍK, L.; ŠEDÝ, M. Utilization of Repeating Substructures for Efficient Representation of Automata (Technical Report). Brno: 2023. p. 1-12. 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. p. 0-0. 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. p. 0-0. 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
Nahoru