As an application of automata theory, the development of high-performance algorithms for Model Checking must guarantee the quality of operation of all new complex systems.
Areas of Expertise
- The algorithmic of omega-automation
These automatons are data structures allowing the represention and reasoning about infinite sets of infinite behaviors. - Temporal logics
The formulas of these logics are used to specify desirable or undesirable behaviors. They use different models of temporal progression to impose constraints between events occurring at different times.
Ongoing research, spotlight on Model Checking
Automatically guarantee the safety of a system
Automatons are data structures that can be used to model all possible behaviors of a physical system, a program, or a protocol. These models can be used to write algorithms that automatically and exhaustively check all possible behaviors of the system: this is Model Checking.
When a model checking tool finds an error, it shows an example of abnormal behavior of the system, and thus allows its correction. Research professors of the Automation and Verification research team are working on improving model checking techniques, which they distribute in the form of free software.
High-tech collaborations
- Laboratoire d’informatique de Paris 6 (Sorbonne Université).
- Faculty of Informatics, Masaryk University (Brno, Czech Republic).
Some major projects
- Spot: Free software for efficient manipulation of automatons and temporal logic formulas.
Participation in the TickTac project funded by the ANR: development of tools for the verification and synthesis of real-time systems.