Lidstvo čím dál více závisí na počítačových systémech, což klade vysoké nároky na jejich bezchybnost a efektivitu. Tyto systémy jsou stále složitější: jejich stavové prostory rostou exponenciálně a současné techniky pro zajištění bezchybnosti neškálují. Chyby se dostávají do reálného nasazení, což způsobuje finanční a lidské ztráty. Tento projekt se zaměřuje na výzkum nových metod pro kompaktní reprezentaci obrovských stavových prostorů těchto systémů. Této kompaktni reprezentace dosáhnu spojením bohaté, ale těžko proniknutelné, teorie automatů a oblastí solverů a formální verifikace, které se zaměřují na výkon v reálných aplikacích. Dané spojení povede k vytvoření nové flexibilní a adaptabilní datové struktury schopné využít vnitřní struktury systémů k jejich kompaktní reprezentaci. Nad datovou strukturou pak vyvinu nástroje schopné manipulovat se stavovými prostory dosud nevídané velikosti. Toto nové paradigma od základů změní pohled na reprezentaci stavových prostorů a bude moci sloužit jako základní technologie pro tvorbu rychlých, bezchybných a bezpečných systémů pro budoucnost.

Description in English
We depend more and more on computer systems, so their correctness and efficiency are of paramount importance. The systems are getting more complex, their state spaces grow exponentially, and techniques for ensuring correctness do not scale. Therefore, bugs often escape into production, causing financial losses or fatalities. This project aims to develop novel methods to compactly handle gigantic state spaces of the systems. For that, I will build a bridge between the rich, but arcane, automata theory, concerned mostly with theoretical questions, and the more down-to-earth areas of solvers and formal verification, focused on real-world performance. In particular, I will connect the two areas to design new flexible and self-adaptable data structures that exploit the internal structure of state spaces for their compact representation. Building on those, I will develop tools able to handle state spaces of unprecedented size. The new paradigm will fundamentally change how state spaces are represented and power the production of fast, safe, and secure computer systems for the future.

Keywords
logiky;modely;binární rozhodovací diagramy;BDD;automaty;kompaktnost;efektivita;formální modely;formální verifikace

Key words in English
logics;models;binary decision diagrams;BDD;automata;compactness;efficiency;formal models;formal verification

GA23-07565S

Czech

Lengál Ondřej, Ing., Ph.D. - principal person responsible
Andriushchenko Roman, Ing. - fellow researcher
Češka Milan, doc. RNDr., Ph.D. - fellow researcher
Dacík Tomáš, Ing. - fellow researcher
Gaďorek Petr, Ing. - fellow researcher
Havlena Vojtěch, Ing., Ph.D. - fellow researcher
Hečko Michal, Ing. - fellow researcher
Chocholatý David, Ing. - fellow researcher
Malásková Věra - fellow researcher
Michal Bohumil, Ing. - fellow researcher
Mrazíková Libuše, Mgr. - fellow researcher
Nesvedová Šárka - fellow researcher
Pirová Zuzana, Ing. - fellow researcher
Rogalewicz Adam, doc. Mgr., Ph.D. - fellow researcher
Šedý Michal, Ing. - fellow researcher
Šmahlíková Barbora, Ing. - fellow researcher
Valová Marie - fellow researcher
Vašíček Ondřej, Ing. - fellow researcher
Ventrubová Hana - fellow researcher

Department of Intelligent Systems
- responsible department (1.4.2022 - not assigned)
Automata@FIT
- internal (1.4.2022 - 31.12.2025)
Department of Intelligent Systems
- beneficiary (1.4.2022 - 31.12.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.; 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

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.; CHOCHOLATÝ, D.; SÍČ, J.; HOLÍK, L.; LENGÁL, O.; CHEN, Y. 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

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

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

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

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

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

Responsibility: Lengál Ondřej, Ing., Ph.D.