Detail projektu
ROULETTE - Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury
Období řešení: 1. 1. 2023 - 31. 12. 2025
Typ projektu: grant
Kód: GA23-07565S
Agentura: Grantová agentura České republiky
Program: Standardní projekty
logiky;modely;binární rozhodovací diagramy;BDD;automaty;kompaktnost;efektivita;formální modely;formální verifikace
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.
Andriushchenko Roman, Ing. (UITS FIT VUT)
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT)
Dacík Tomáš, Ing. (UITS FIT VUT)
Gaďorek Petr, Ing. (DFIT-OIP)
Havlena Vojtěch, Ing., Ph.D. (UITS FIT VUT)
Hečko Michal, Ing. (UITS FIT VUT)
Chocholatý David, Ing. (FIT VUT)
Malásková Věra (UITS FIT VUT)
Michal Bohumil, Ing. (CVT FIT VUT)
Mrazíková Libuše, Mgr. (Děkanát FIT VUT)
Nesvedová Šárka (Děkanát FIT VUT)
Pirová Zuzana, Ing. (Děkanát FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Šedý Michal, Ing. (FIT VUT)
Šmahlíková Barbora, Ing. (UITS FIT VUT)
Valová Marie (Děkanát FIT VUT)
Vašíček Ondřej, Ing. (UITS FIT VUT)
Ventrubová Hana (Děkanát FIT VUT)
2025
- ABDULLA Parosh A., CHEN Yo-ga, CHEN Yu-Fang, HOLÍK Lukáš, LENGÁL Ondřej, LIN Jyun-ao, LO Fang-yi a TSAI Wei-lun. Verifying Quantum Circuits with Level-Synchronized Tree Automata. Proceedings of the ACM on Programming Languages, roč. 9, č. 1, 2025, s. 923-953. ISSN 2475-1421. Detail
- CHOCHOLATÝ David, HAVLENA Vojtěch, HOLÍK Lukáš, HRANIČKA Jan, LENGÁL Ondřej a SÍČ Juraj. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. In: Proceedings of TACAS'25. Hamilton: Springer Verlag, 2025, s. 22. ISSN 0302-9743. Detail
2024
- HABERMEHL Peter, HAVLENA Vojtěch, HEČKO Michal, HOLÍK Lukáš a LENGÁL Ondřej. Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. In: Proceedings of CAV'24. Montreal: Springer Verlag, 2024, s. 42-67. ISSN 0302-9743. Detail
- HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej a SÍČ Juraj. Cooking String-Integer Conversions with Noodles. In: Proceedings of SAT'24. Leibniz International Proceedings in Informatics (LIPIcs). Pune: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2024, s. 1-19. ISSN 1868-8969. 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
- HAVLENA Vojtěch, HOLÍK Lukáš, CHEN Yu-Fang, CHOCHOLATÝ David, LENGÁL Ondřej a SÍČ Juraj. Z3-Noodler: An Automata-based String Solver. In: Proceedings of TACAS'24. Lecture Notes. Luxembourgh: Springer Verlag, 2024, s. 24-33. ISSN 0302-9743. Detail
2023
- 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
- 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
- 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
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