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
Češka Milan, doc. RNDr., Ph.D. (UITS)
Dacík Tomáš, Ing. (UITS)
Havlena Vojtěch, Ing., Ph.D. (UITS)
Chocholatý David, Ing. (UITS)
Malásková Věra (UITS)
Michal Bohumil, Ing. (CVT)
Mrazíková Libuše, Mgr. (DFIT-PO)
Pirová Zuzana, Ing. (DFIT-EO)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Šedý Michal, Ing. (UITS)
Vašíček Ondřej, Ing. (UITS)
Publikace

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
  • 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, 2024. p. 0-0. ISBN: 979-8-4007-1077-3. 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
Nahoru