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
2014–2018
ongoing
ANR
🇫🇷
PACS
Parametric analyses of concurrent systems
PI 8 450k€
2018
ongoing
DIM RFSI
🇫🇷
ASTREI
Analyse de systèmes temps-réel modélisés par Time4sys en présence d’incertitude
PI 1 10k€
2014–2015 CNRSPAN
🇫🇷 🇵🇱
BehaPPi-BMC
Behavior preserving parametric bounded model checking
co-PI 4 8k€
2014 BQR
🇫🇷
SynPaTiC
Synthèse de paramètres temporels distribuée et multi-cœurs
PI 2 15k€
2013 Actions émergentes GDR GPL
🇫🇷
IOP
Intégration d’outils à la plate-forme CosyVerif
PI 1 2k€
2012–2014 PHC Merlion
🇫🇷 🇸🇬
BRAVOS
Software Verification from Design to Implementation
co-PI 6 30k€
Total 515k€

Project participant

Year Call Project name PI Permanent staff Budget
2015 PEPS JCJC
🇫🇷
PSyCoS
Parallel SYnthesis for COncurrent Systems
Camille Coti 2 10k€
2013–2014 STIC Asie
🇫🇷 🇸🇬 🇻🇳
CATS
Compositional analysis of timed systems
Laure Petrucci 6 34k€
2013 PHC Merlion
🇫🇷 🇸🇬
FSFMA
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
🇫🇷
VALMEM
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
🇫🇷
SIMOP
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

PAT

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

Developer

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

PSyHCoS

Developer

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

InSPEQTor

Developer

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

ImpRator

Developer

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

Students

Post-docs

Louis Fippo-Fitime (2017—…)

Louis Fippo Fitime Parametric analyses of biological systems

PhD students

Mathias Ramparison

(2016—…)

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

Nguyễn Hoàng Gia

(2015—…)

Nguyễn Hoàng Gia Efficient and distributed parameter synthesis for parametric timed automata
Co-supervised by Laure Petrucci

Mohamed Mahdi Benmoussa

(2013—2016)

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

Romain Soulat

(2010—2013)

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

Education

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.

Contact

Affiliation

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
France

E-Mail address

Etienne.Andre(at)univ-paris13.fr

Phone

Please send me an email first

Fax

…in 2017…? like seriously…?

ha-index

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