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.
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT)
Havlena Vojtěch, Ing., Ph.D. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
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, 2023. ISSN 2475-1421. 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