Project Details

Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury

Project Period: 1. 1. 2023 – 31. 12. 2025

Project Type: grant

Code: GA23-07565S

Agency: Czech Science Foundation

Program: Standardní projekty

English title
Representing Boolean Functions by a Self-Adaptable Data Structure
Type
grant
Keywords

logics;models;binary decision diagrams;BDD;automata;compactness;efficiency;formal
models;formal verification

Abstract

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.

Team members
Lengál Ondřej, Ing., Ph.D. (DITS) – research leader
Andriushchenko Roman, Ing. (DITS)
Češka Milan, doc. RNDr., Ph.D. (DITS)
Dacík Tomáš, Ing. (DITS)
Gaďorek Petr, Ing. (DFIT-ISD)
Havlena Vojtěch, Ing., Ph.D. (DITS)
Hečko Michal, Ing. (DITS)
Chocholatý David, Ing. (DITS)
Malásková Věra (DITS)
Michal Bohumil, Ing. (CVT)
Mrazíková Libuše, Mgr. (DFIT-PO)
Nesvedová Šárka (DFIT-PO)
Pirová Zuzana, Ing. (DFIT-FO)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Šedý Michal, Ing. (DITS)
Šmahlíková Barbora, Ing. (RG VERIFIT)
Valová Marie (DFIT-PO)
Vašíček Ondřej, Ing. (DITS)
Ventrubová Hana (DFIT-FO)
Publications

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

  • 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
  • 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
  • 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
Back to top