Étienne André

Full professor @ Sorbonne Paris Nord (he, him)

Member of the Institut Universitaire de France (2024-2029)

I am full professor within Université Sorbonne Paris Nord. I belong to the LoVe research team at LIPN.

I support the manifesto for sustainable research in theoretical computer science, notably through the reduction of our carbon footprint and (therefore) our plane travels.

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 monitoring cyber-physical systems, and in detecting side-channel attacks using quantitative formal methods.

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

Latest works

Verifying Timed Properties of Programs in IoT nodes using Parametric Time Petri Nets

Latest publication

Étienne André, Jean-Luc Béchennec, Sudipta Chattopadhyay, Sébastien Faucou, Didier Lime, Dylan Marinho, Olivier H. Roux and Sun Jun. Verifying Timed Properties of Programs in IoT nodes using Parametric Time Petri Nets. In Justyna Petke, Anton Wijs, Juw Won Park and Adam Przybylek (eds.), SAC’25, ACM/IEEE, March 2025. To appear. (English)

See all publications

Latest talk

4th December 2024: Tuning Trains Speed in Railway Scheduling (ICFEM’24, 🇯🇵 Hiroshima)

See all talks

Research projects

Project PI

Year	Call	Project name	Role	Permanent staff	Budget
2024 ongoing	PHC Polonium 🇫🇷 🇵🇱	MoCcA Analyses of multi-agent systems	PI	6	3k€ (*2)
2020–2024 ongoing	ANR-NRF 🇫🇷 🇸🇬	ProMiS Provable Mitigation of Side Channel through Parametric Verification	PI	5	276k€ (*2)
2020	IFD 🇫🇷 🇩🇰	SECReTS Synthesis of Energy-optimal Constraints for REal-Time Systems	PI	4	3k€
2014–2019	ANR 🇫🇷	PACS Parametric analyses of concurrent systems	PI	8	450k€
2018	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	CNRS–PAN 🇫🇷 🇵🇱	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€

Project participant

Year	Call	Project name	PI	Permanent staff	Budget
2023–2027	ANR 🇫🇷	BisoUS	Didier Lime	15	409k€
2018–2019	ERATO 🇯🇵	MMSD Metamathematics for Systems Design	Ichiro Hasuo (蓮尾一郎)	>20	10000k€
2019–2020	PICS 🇫🇷 🇵🇱	PARTIES verification of PARametric TIme constrained strategic abilitiES for agents acting under incomplete information	Laure Petrucci	7	8k€
2018–2019	PHC Van Gogh 🇫🇷 🇳🇱	PAMPAS Parallel algorithms for model-checking and parameter synthesis	Laure Petrucci	11	7k€
2018	BQR 🇫🇷	AMoJAS Arbres attaque-défense et Modèles de Jeux pour l’Analyse de la Sécurité	Laure Petrucci	7	6k€
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

Program committees

2026

🇮🇹TACAS 2026

2025

🇺🇸HSCC 2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

Steering committees

SynCoP: 2016, 2017, 2018, 2019, 2022, 2023, 2024.
MeFoSyLoMa (2017-2019, 2023-…)
Petri Nets (2024-…)

Conference organization

Petri Nets 2025 (co-general chair)
ETAPS 2023 (proceedings chair + Extended Stay Support Scheme organizer)
Petri Nets 2021 (co-general chair)
Petri Nets 2020 @ Paris Nord Summer of LoVe (co-general chair)
ICFEM 2015 (workshop chair)
FSFMA 2014 (co-general chair)

PhD theses reviewer

Year	Phd student	Institution
2024	Yushi Cao	Nanyang Technological University, Singapore 🇸🇬
2024	Tomáš Kolárik	Czech technical university in Prague 🇨🇿
2023	Akshay Mambakam	Université Grenoble Alpes 🇫🇷
2022	Bastien Serée	École Centrale Nantes
2021	Léo Henry	Université de Rennes 1
2020	Clément Bertrand	Université d’Evry, Université Paris-Saclay 🇫🇷
2020	Victor Roussanaly	Université de Rennes 1
2020	Jiao Jiao	Nanyang Technological University, Singapore 🇸🇬
2019	Du Xiaoning	Nanyang Technological University, Singapore 🇸🇬
2018	Wang Junjie	Nanyang Technological University, Singapore 🇸🇬
2018	Chandramohan Mahinthan	Nanyang Technological University, Singapore 🇸🇬
2017	Wu Zhimin	Nanyang Technological University, Singapore 🇸🇬
2013	Zhu Huiquan	National University of Singapore 🇸🇬

Scientific expert

Year	Institution
2020	🇯🇵	EIG CONCERT-Japan
2015, 2016	🇫🇷	Agence nationale de la recherche
2014	🇳🇱	Nederlandse Organisatie voor Wetenschappelijk Onderzoek

Software development

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.

Open source

IMITATOR is entirely open-source and is distributed under the GNU General Public License.

More on IMITATOR…

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).

HyMITATOR

Developer

HyMITATOR is a fork of IMITATOR for parametric hybrid automata.

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

PhD students

Sarah Dépernet

(2024-…)

Verifying timed cybersecurity properties using formal methods
Co-supervised by Engel Lefaucheux

Dylan Marinho

(2020-2023)

Detecting timed attacks using formal methods
🏆 PhD award 2024 from Académie Lorraine des Sciences (France)
Current situation: Associate professor with Sorbonne Université (France)

Jawher Jerray

(2018-2021)

Formal analyses of real-time systems
Co-supervised by Laurent Fribourg
Current situation: Associate professor with Université de Pau (France)

Mathias Ramparison

(2016-2019)

Formal verification of parametric real-time systems with preemption
Co-supervised by Didier Lime
Current situation: Associate professor in INP Grenoble (France)

Nguyễn Hoàng Gia

(2015-2018)

Efficient and distributed parameter synthesis for parametric timed automata
Co-supervised by Laure Petrucci
Current situation: Post-doc at CEA (France)

Mohamed Mahdi Benmoussa

(2013-2016)

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

Romain Soulat

(2010-2013)

Synthesis of correct-by-design schedulers for hybrid systems
Co-supervised by Laurent Fribourg
Current situation: Technical Lead for Certification, Input Output

Post-docs

Emily Clement (2024-…)

Monitoring cyber-physical systems

Laetitia Laversa (2023-2024)

Controlling opacity in timed systems
Co-supervised by Marie Duflot, Engel Lefaucheux

Johan Arcile (2020-2022)

Detecting timing attacks using formal methods
Current situation: Associate professor with Université Paris-Saclay (France)

Master students

Name	Year
Sarah Dépernet	2024
Shapagat Bolat	2022
Aleksander Kryukov	2020
Jawher Jerray	2018
Sahar Mhiri	2018
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

Full professor

I have been from 2019 to 2022 full professor with Université de Lorraine, member of the VeriDis research team of LORIA.

Associate professor

I have been from 2011 to 2019 an associate professor in the LoVe team of LIPN with Université Sorbonne Paris Nord (formerly "Paris 13").

Post-doctoral activity

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.