Theoretical Computer Science
The Theoretical Computer Science group focuses on theories, methods and tools for the rigorous design of reliable, safe, and efficient software and computer systems.
ts first line of research studies symbolic state-space exploration, which verifies computer systems by examining their possible executions in a symbolical way. This approach calls for powerful algorithms and data structures for computing the state space for various kinds of models, and in particular those that have infinitely many reachable configurations. Another objective is to study the theoretical properties of symbolic data structures based on finite-state automata and logical formulas. The second line of research, connected to the first, relates to the satisfiability checking problem for large logical formulas, in particular those expressed in a combination of theories. Its main goal consists in engineering tools known as Satisfiability Modulo Theories (SMT) solvers, whose application field spans several areas of computer
science, including verification.