Project Details

ROULETTE - 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. (UITS FIT VUT) , research leader
Andriushchenko Roman, Ing. (UITS FIT VUT)
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT)
Dacík Tomáš, Ing. (UITS FIT VUT)
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)
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)
Vašíček Ondřej, Ing. (UITS FIT VUT)
Publications

2024

  • CHEN Tian-fu, CHEN Yu-Fang, JIANG Jie-hong, JOBRANOVÁ Sára and LENGÁL Ondřej. Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization. In: IEEE/ACM International Conference on Computer-Aided Design (ICCAD '24), October 27--31, 2024, New York, NY, USA. Association for Computing Machinery, 2024. ISBN 979-8-4007-1077-3. Detail
  • HABERMEHL Peter, HAVLENA Vojtěch, HEČKO Michal, HOLÍK Lukáš and LENGÁL Ondřej. Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. In: Proceedings of CAV'24. Montreal: Springer Verlag, 2024, pp. 42-67. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and 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, pp. 1-19. ISSN 1868-8969. Detail
  • FIEDOR Tomáš, HAVLENA Vojtěch, HOLÍK Lukáš, HRUŠKA Martin, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Mata: A Fast and Simple Finite Automata Library. In: Proceedings of TACAS'24. Luxembourgh: Springer Verlag, 2024, pp. 130-151. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, HOLÍK Lukáš, CHEN Yu-Fang, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Z3-Noodler: An Automata-based String Solver. In: Proceedings of TACAS'24. Lecture Notes. Luxembourgh: Springer Verlag, 2024, pp. 24-33. ISSN 0302-9743. Detail

2023

  • CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao, TSAI Wei-lun and YEN Di-de. An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. Proceedings of the ACM on Programming Languages, vol. 7, no. 6, 2023, pp. 1218-1243. ISSN 2475-1421. Detail
  • CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao and TSAI Wei-lun. AutoQ: An Automata-based Quantum Circuit Verifier. In: Proceedings of 35th International Conference on Computer Aided Verification. Cham: Springer Verlag, 2023, pp. 139-153. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej, LI Yong, ŠMAHLÍKOVÁ Barbora and TURRINI Andrea. Modular Mix-and-Match Complementation of Büchi Automata. In: Proceedings of TACAS'23. Paris: Springer Verlag, 2023, pp. 249-270. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej, LI Yong, ŠMAHLÍKOVÁ Barbora and 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 and SÍČ Juraj. Solving String Constraints with Lengths by Stabilization. Proceedings of the ACM on Programming Languages, vol. 7, no. 10, 2023, pp. 2112-2141. ISSN 2475-1421. Detail
Products

2024

  • Mata: A Finite Automata Library, software, 2024
    Authors: Fiedor Tomáš, Havlena Vojtěch, Holík Lukáš, Hruška Martin, Chocholatý David, Lengál Ondřej, Síč Juraj Detail
  • Z3-Noodler: A String Solver, software, 2024
    Authors: Havlena Vojtěch, Holík Lukáš, Chen Yu-Fang, Chocholatý David, Lengál Ondřej, Síč Juraj Detail
Back to top