Team presentation

Computer systems play a central role in modern societies and their
errors can have dramatic consequences. Industry and academics thus
invest a considerable amount of effort developing techniques to prove
the correctness of these systems. Among such techniques, one finds (1)
testing, the traditional approach to detect bugs with test
cases, and (2) formal methods, e.g., model checking (Turing
award), that can guarantee the absence of bugs.
Both approaches have been largely deployed on static systems, whose
behaviour is entirely known. ESTASYS focuses on developping
brand new formal methods for Systems of Systems.

Research themes

Formal verification

Statistical Model Checking

Variability analysis

Quantitative modeling.

International and industrial relations

Aalborg University

Université de Namur




University of Trento

Rice University

University of Copenhagen

Université de Vannes

Aachen University

Lerho (Ireland)

University of Dortmund

University of Vienna

Royal Holloway University of London

ESTASYS is an exploratory action and Inria team that proposes inovative techniques for the rigorous design of Cyber Physical Systems (CPS). ESTASYS focuses on :

  • New efficient simulation techniques used to overcome both the undecidability and state-space explosion problems
  • New quantitative techniques to reason on complex properties such as resource allocation and energy budget.
  • New techniques to quantify privacy and information flow (secure passwords, etc)
  • New revolutiony tools and integrated libraries.
  • New contract theories for requirement specifications.