Model-checking et synthèse


Add suggestions/comments/discussion here:

Older discussion:

We could add the list of members (Patricia) - done

What about games? Could we have this notion explicitly in the topics? (Patricia) - done

Removed Concurrency as it is covered by the team Concurrence et distribué (Laurent D)


We are interested in the foundations of computation. Formal models of computation include classes of languages and machines such as finite automata, games, pushdown and counter systems, weighted automata, (continuous) timed systems, stochastic processes. We identify and study fundamental properties of these models, such as expressiveness, computational complexity, succinctness, equivalence among different models.

We embed our study into rigorous mathematical framework rooted with formal logic, and develop algorithmic procedures, either to prove the correctness of a model, or to provide a counter-example. We develop decision procedures for solving fundamental questions related to the models and logics (satisfiability, realizability, optimization) and provide complexity lower and upper bounds (time and space).

Our goal is to provide efficient techniques and tools to automate and optimize the design of systems (software, circuits, etc.). We seek to establish the correctness of systems through the approaches of verification, diagnosis, learning, control, and synthesis. Furthermore, we develop quantitative approaches to optimize the quality of designed systems.


  • Formal models of computation
    • Finite/Infinite
    • Boolean/Quantitative
    • Real-time/Partial information/Stochasticity
    • Games
  • Logic & decision problems
    • Expressiveness
    • Satisfiability/Realizability
    • Satisfiability modulo theories (SMT)
    • Decidability/Complexity
  • Automated system design
    • Tools/prototypes
    • Applications: Software verification, diagnosis, learning, control, synthesis

Permanent members

Non-permanent members

PhD students:

  • Georges Aazan (L. Fribourg & A. Girard)
  • Ashwin Bhaskar (S. Demri)
  • Benjamin Bordais (P. Bouyer & S. Le Roux)
  • Mathieu Hilaire (B. Bollig & S. Göller)
  • Jawher Jerray (L. Fribourg & E. André)
  • Igor Khmelnitsky (A. Finkel & S. Haddad)
  • Sayan Mukerjee (P. Gastin & B. Srivathsan)
  • Olivier Stietel (B. Bollig & A. Sangnier)
  • Amrita Suresh (B. Bollig & A. Finkel)
  • Nathan Thomasset (P. Bouyer & S. Le Roux)
  • Pierre Vandenhove (P. Bouyer & M. Randour)

Post-doctoral students:

  • Raine Rönnholm (D. Berwanger)

Associated Staff:

  • Philippe Dague (Emeritus Professor)


Groupe de Travail

Page du Groupe de Travail MCS

Version française