I am interested in specifying and formally verifying concurrent systems. My research focuses especially on verification of timed systems (or real-time systems) under uncertainty, i.e., with timing parameters, and notably on parametric timed model-checking. I am also interested in compositional verification, and in specifying systems using formal extensions of the UML.

Keywords: model checking, Verification, distributed and concurrent systems, Timed systems, Parametric Timed Automata, Parameter synthesis.

Latest works

Latest publication

Latest publication

Étienne André, Nguyễn Hoàng Gia and Laure Petrucci. Efficient parameter synthesis using optimized state exploration strategies. In Zhenjiang Hu and Guangdong Bai, (eds.), ICECCS’17, IEEE CPS, November 2017. Acceptance rate: 40%. To appear. (English)

Research projects

Project PI

Year Call Project name Role Permanent staff Budget
Parametric analyses of concurrent systems
PI 8 450k€
2014–2015 CNRSPAN
🇫🇷 🇵🇱
Behavior preserving parametric bounded model checking
co-PI 4 8k€
2014 BQR
Synthèse de paramètres temporels distribuée et multi-cœurs
PI 2 15k€
2013 Actions émergentes GDR GPL
Intégration d’outils à la plate-forme CosyVerif
PI 1 2k€
2012–2014 PHC Merlion
🇫🇷 🇸🇬
Software Verification from Design to Implementation
co-PI 6 30k€
Total 505k€

Project participant

Year Call Project name PI Permanent staff Budget
Parallel SYnthesis for COncurrent Systems
Camille Coti 2 10k€
2013–2014 STIC Asie
🇫🇷 🇸🇬 🇻🇳
Compositional analysis of timed systems
Laure Petrucci 6 26k€
2013 PHC Merlion
🇫🇷 🇸🇬
French Singaporean Workshop on Formal Methods and Applications
Christine Choppy + Sun Jun 9 8k
2010 PHC Galilée
🇫🇷 🇮🇹
Synthèse et contraintes Laurent Fribourg 3 12k€
2007–2010 ANR
Validation fonctionnelle et temporelle des mémoires embarquées, décrites au niveau transistor, par des méthodes formelles
Laurent Fribourg 7 572k€
2007–2009 Institut Farman
Simulation et model-checking paramétré
Laurent Fribourg 6 20k€

Program committees and evaluations

Software development

Behavioral cartography by IMITATOR

IMITATOR: parameter synthesis for real-time systems

I initated the development of IMITATOR in 2008, and I am since then the lead developer.

IMITATOR is a software to synthesize timing parameters for concurrent timed systems modeled using extensions of parametric timed automata.

IMITATOR was used in several industrial collaborations on hardware verification, and schedulability analysis under uncertainty.

An expressive input language

IMITATOR performs parameter synthesis for real-time systems modeled by an extension of parametric timed automata.

Powerful analyses

Various algorithms are implemented in IMITATOR, including safety parameter synthesis, deadlock-freeness, non-Zeno parametric model-checking or robustness analysis.

Graphical outputs

In addition to results output using predefined formats, IMITATOR generates graphical outputs such as the zones of good behaviors for the timing parameters.

Other software


Member of the development team (2010-2013)

PAT is a powerful model-checker for multiple formalisms such as timed CSP, probabilistic systems, parametric systems… PAT is mainly developed in Singapore (NUS, STUD, NTU).



PolyOp is a simple interface to some operations on polyhedra provided by the Parma Polyhedra Library.



PSyHCoS is tool that groups techniques of parameter synthesis for Parametric Stateful Timed CSP (PSTCSP).



InSPEQTor is an implementation of the inverse method in the framework of Parametric Directed Weighted Graphs.



ImpRator is an implementation of the inverse method in the framework of Parametric Markov Decision Processes.



Louis Fippo-Fitime (2017—…)

Louis Fippo Fitime Parametric analyses of biological systems

PhD students

Mathias Ramparison


Formal verification of parametric real-time systems with preemption
Co-supervised by Didier Lime

Nguyễn Hoàng Gia


Efficient and distributed parameter synthesis for parametric timed automata
Co-supervised by Laure Petrucci

Mohamed Mahdi Benmoussa


Specification with the UML
Co-supervised by Christine Choppy
Current situation: Assistant professor in Constantine (Algeria)

Romain Soulat


Romain Soulat Synthesis of correct-by-design schedulers for hybrid systems
Co-supervised by Laurent Fribourg
Current situation: R&D engineer with Thales (France)

Master students

Name Year
Mathias Ramparison 2016
Nguyễn Hoàng Gia 2014
Christopher Makanga 2014
Mohamed Mahdi Benmoussa 2013
Taieb Ben Niha 2013
Giuseppe Pellegrino 2012−2013
Shweta Garg (श्वॆता) 2012
Inès Jguirim 2012
Daphné Dussaud 2010
Sandeep Grewal 2008


Post-doctoral activity

National University of Singapore

I have been from December 2010 to August 2011 a research fellow (post-doc) in Prof. Dong Jin Song (董劲松)’s team in the National University of Singapore.
I keep collaborating with several Singapore-based scientists.



Université Paris 13, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France

Snail mail address

Étienne André
Laboratoire d’Informatique de Paris-Nord
Institut Galilée
Université Paris 13
99 avenue Jean-Baptiste Clément
93430 Villetaneuse

E-Mail address



Please send me an email first


…in 2017…? like seriously…?


I am very proud that my ha-index is 78.