ω-Automata
ω-Automata are automata which recognize infinite words. They are used in various applications such as model checking, where one tests whether an ω-automaton which models the behavior of the system intersects another ω-automaton which represents undesirable properties, and the synthesis of reactive controllers, which involves building systems that generate output signals in response to input signals, while satisfying a specification that constrains the relation between them. The group develops and maintains the tool Spot, a library for manipulation of ω-automata.
Fundations of concurrency theory
Higher-dimensional automata (HDAs) are automata which may be used to reason about concurrent and distributed computations. The group develops the theory of these HDAs and their relations with other models for concurrent and distributed systems.
Automated reasoning
Automated reasoning focuses on the development and application of logical methods for the analysis, verification, and synthesis of systems. It encompasses SAT-based techniques, theorem proving, but also constraint programming, abstract interpretation and model learning.