Skip to content
Meet us on our different events

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.
Retour en haut de page