Detail projektu

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

Název anglicky
Representing Boolean Functions by a Self-Adaptable Data Structure
Typ
grant
Klíčová slova

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

Abstrakt

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šitelé
Lengál Ondřej, Ing., Ph.D. (UITS) – hlavní řešitel
Andriushchenko Roman, Ing. (UITS)
Češka Milan, doc. RNDr., Ph.D. (UITS)
Dacík Tomáš, Ing. (UITS)
Gaďorek Petr, Ing. (DFIT-OIP)
Havlena Vojtěch, Ing., Ph.D. (UITS)
Hečko Michal, Ing. (UITS)
Chocholatý David, Ing. (UITS)
Malásková Věra (UITS)
Michal Bohumil, Ing. (CVT)
Mrazíková Libuše, Mgr. (DFIT-PO)
Nesvedová Šárka (DFIT-PO)
Pirová Zuzana, Ing. (DFIT-EO)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Šedý Michal, Ing. (UITS)
Šmahlíková Barbora, Ing. (VZ VERIFIT)
Valová Marie (DFIT-PO)
Vašíček Ondřej, Ing. (UITS)
Ventrubová Hana (DFIT-EO)
Publikace

2026

  • 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, 2026. ISBN: 979-8-4007-1077-3. Detail

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
  • CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; HRANIČKA, J.; LENGÁL, O.; SÍČ, J. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. Proceedings of TACAS'25. Lecture Notes in Computer Science. Hamilton: Springer Verlag, 2025. ISSN: 0302-9743. Detail

2024

  • 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.; 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.; 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

2023

  • 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
  • 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
Produkty

2024

Nahoru