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

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 FIT VUT) , hlavní řešitel
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)

Publikace

2024

DACÍK Tomáš, ROGALEWICZ Adam, VOJNAR Tomáš a ZULEGER Florian. Deciding Boolean Separation Logic via Small Models. In: 2024. Detail
FIEDOR Tomáš, HAVLENA Vojtěch, HOLÍK Lukáš, HRUŠKA Martin, CHOCHOLATÝ David, LENGÁL Ondřej a SÍČ Juraj. Mata: A Fast and Simple Finite Automata Library. In: Proceedings of TACAS'24. Luxembourgh: Springer Verlag, 2024, s. 130-151. ISSN 0302-9743. Detail

2023

HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej a TURRINI Andrea. A symbolic algorithm for the case-split rule in solving word constraints with extensions. Journal of Systems and Software, roč. 201, č. 201, 2023, s. 111673-111693. ISSN 0164-1212. Detail
CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao, TSAI Wei-lun a YEN Di-de. An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. Proceedings of the ACM on Programming Languages, roč. 7, č. 6, 2023, s. 1218-1243. ISSN 2475-1421. Detail
CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao a TSAI Wei-lun. AutoQ: An Automata-based Quantum Circuit Verifier. In: Proceedings of 35th International Conference on Computer Aided Verification. Cham: Springer Verlag, 2023, s. 139-153. ISSN 0302-9743. Detail
ANDRIUSHCHENKO Roman, BARTOCCI Ezio, ČEŠKA Milan, FRANCESCO Pontiggia a 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), roč. 14287. Cham: Springer Verlag, 2023, s. 288-306. ISBN 978-3-031-43834-9. Detail
HOLÍK Lukáš, HOLÍKOVÁ Lenka, SÍČ Juraj a VOJNAR Tomáš. Fast Matching of Regular Patterns with Synchronizing Counting. In: Foundations of Software Science and Computation Structures. Heidelberg: Springer Verlag, 2023, s. 392-412. ISSN 0302-9743. Detail
HOLÍK Lukáš, HOLÍKOVÁ Lenka, SÍČ Juraj a 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 a TURRINI Andrea. Modular Mix-and-Match Complementation of Büchi Automata. In: Proceedings of TACAS'23. Paris: Springer Verlag, 2023, s. 249-270. ISSN 0302-9743. Detail
HAVLENA Vojtěch, LENGÁL Ondřej, LI Yong, ŠMAHLÍKOVÁ Barbora a 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 a VARGOVČÍK Pavol. Reasoning about Regular Properties: A Comparative Study. In: Automated Deduction - CADE 29. Cham: Springer Nature Switzerland AG, 2023, s. 286-306. ISSN 0302-9743. Detail
CHEN Yu-Fang, CHOCHOLATÝ David, HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej a SÍČ Juraj. Solving String Constraints with Lengths by Stabilization. Proceedings of the ACM on Programming Languages, roč. 7, č. 10, 2023, s. 2112-2141. ISSN 2475-1421. Detail
HOLÍK Lukáš a Š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 a SÍČ Juraj. Word Equations in Synergy with Regular Constraints. In: Proceedings of FM'23. Lübeck: Springer Verlag, 2023, s. 403-423. ISSN 0302-9743. Detail

2022

HAVLENA Vojtěch, LENGÁL Ondřej a ŠMAHLÍKOVÁ Barbora. Complementing Büchi Automata with Ranker. In: Proceedings of the 34th International Conference on Computer Aided Verification. Haifa: Springer Verlag, 2022, s. 188-201. ISBN 978-3-031-13187-5. ISSN 0302-9743. Detail
HAVLENA Vojtěch, LENGÁL Ondřej a Š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 a 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, s. 112-125. ISSN 2075-2180. Detail
HOLÍKOVÁ Lenka, HOLÍK Lukáš, HOMOLIAK Ivan, LENGÁL Ondřej, VEANES Margus a 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, s. 4165-4182. ISBN 978-1-939133-31-1. Detail
HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš a ZULEGER Florian. Low-Level Bi-Abduction. In: 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics, roč. 2022. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2022, s. 1-30. ISBN 978-3-95977-225-9. ISSN 1868-8969. Detail
HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš a ZULEGER Florian. Low-Level Bi-Abduction (Artifact). Dagstuhl, 2022. Detail
HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš a ZULEGER Florian. Low-Level Bi-Abduction (technical report). Ithaca, 2022. Detail
HAMMER Jan a 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, s. 88-111. ISSN 2075-2180. Detail
GE-ERNST Aile, SCHOLL Christoph, SÍČ Juraj a WIMMER Ralf. Solving dependency quantified Boolean formulas using quantifier localization. Theoretical Computer Science, roč. 2022, č. 925, s. 1-24. ISSN 0304-3975. Detail

2021

SÍČ Juraj a 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, s. 535-544. ISSN 0302-9743. Detail
MATOUŠEK Petr, HAVLENA Vojtěch a 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, s. 81-89. ISBN 978-3-903176-32-4. Detail
KŘIVKA Zbyněk a MEDUNA Alexander. Scattered Context Grammars with One Non-Context-Free Production are Computationally Complete. Fundamenta Informaticae, roč. 179, č. 4, 2021, s. 361-384. ISSN 0169-2968. Detail
ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang a 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, s. 305-320. ISBN 978-3-030-89051-3. Detail

2020

HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej a TURRINI Andrea. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In: Proceedings of APLAS'20. Heidelberg: Springer Verlag, 2020, s. 343-363. ISSN 0302-9743. Detail
HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej, VALEŠ Ondřej a VOJNAR Tomáš. Antiprenexing for WSkS: A Little Goes a Long Way. In: EPiC Series in Computing. Proceedings of LPAR-23. Manchester: EasyChair, 2020, s. 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 a 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, s. 943-957. ISBN 978-1-4503-7613-6. Detail
HOLÍKOVÁ Lenka, HOLÍK Lukáš, LENGÁL Ondřej, SAARIKIVI Olli, VEANES Margus a VOJNAR Tomáš. Regex Matching with Counting-Set Automata. Proceedings of the ACM on Programming Languages, roč. 4, č. 11, 2020, s. 1-30. ISSN 2475-1421. Detail

Produkty

2024

Mata: Knihovna pro konečné automaty, software, 2024
Autoři: Fiedor Tomáš, Havlena Vojtěch, Holík Lukáš, Hruška Martin, Chocholatý David, Lengál Ondřej, Síč Juraj Detail
Z3-Noodler: Řetězcový Řešič, software, 2024
Autoři: Havlena Vojtěch, Holík Lukáš, Chen Yu-Fang, Chocholatý David, Lengál Ondřej, Síč Juraj Detail

2022

Broom: Nástroj pro statickou analýzu C programů založen na separační logice a bi-abdukčním přístupu, software, 2022
Autoři: Holík Lukáš, Peringer Petr, Rogalewicz Adam, Šoková Veronika, Vojnar Tomáš, Zuleger Florian Detail
GadgetCA - Nástroj pro generování ReDoS útoků, software, 2022
Autoři: Holík Lukáš, Holíková Lenka, Homoliak Ivan, Lengál Ondřej, Veanes Margus, Vojnar Tomáš Detail
Ranker: Nástroj pro komplementaci Büchiho automatů, software, 2022
Autoři: Havlena Vojtěch, Lengál Ondřej, Šmahlíková Barbora Detail