Automation and Application

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.

Automation and Application

Areas of Expertise

Ongoing research, spotlight on Model Checking

High-tech collaborations

Some major projects