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

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


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


Back to top