Étienne André

Professeur @ Sorbonne Paris Nord (il, lui)

Membre de l’Institut Universitaire de France (2024-2029)

Je suis professeur à l’Université Sorbonne Paris Nord : chercheur dans l’équipe LoVe du LIPN, et enseignant en informatique à l’Institut Galilée.

Je soutiens le manifeste pour une recherche durable en informatique théorique, notamment par la réduction de notre bilan carbone et (donc) par la forte diminution de nos déplacements en avion (prenons le train !).

Je m’intéresse à la spécification et à la vérification formelle de systèmes distribués, notamment temporisés. Ma recherche porte particulièrement sur la vérification de systèmes temporisés (voire temps-réel) en présence de paramètres temporels, et notamment au model-checking paramétré. Je m’intéresse également au monitoring de systèmes cyber-physiques, ainsi qu’à la détection d’attaques par canaux cachés à l’aide de model-checking quantitatif.

Mots-clés : model-checking, vérification, systèmes concurrents et distribués, systèmes temporisés, automates temporisés paramétrés, synthèse de paramètres.

Derniers travaux

Dernière publication

Étienne André, Sarah Dépernet et Engel Lefaucheux. The Bright Side of Timed Opacity. Sous la direction de Kazuhiro Ogata, Meng Sun and Dominique Méry (éditeurs), ICFEM’24, Springer LNCS, décembre 2024. À paraître. (English)

Voir toutes les publications

Dernier exposé

23 avril 2023 : Configuring timing parameters to ensure opacity (TiCSA’23, 🇫🇷 Paris)

Voir tous les exposés

Projets de recherche

Porteur de projets

Année	Appel	Nom du projet	Rôle	Membres	Budget
2024 en cours	PHC Polonium 🇫🇷 🇵🇱	MoCcA Analyses of multi-agent systems	Porteur	6	3k€ (*2)
2020–2024 en cours	ANR-NRF 🇫🇷 🇸🇬	ProMiS Provable Mitigation of Side Channel through Parametric Verification	Porteur	5	276k€ (*2)
2020	IFD 🇫🇷 🇩🇰	SECReTS Synthesis of Energy-optimal Constraints for REal-Time Systems	Porteur	4	3k€
2014–2019	ANR 🇫🇷	PACS Parametric analyses of concurrent systems	Porteur	8	450k€
2018	DIM RFSI 🇫🇷	ASTREI Analyse de systèmes temps-réel modélisés par Time4sys en présence d’incertitude	Porteur	1	10k€
2014–2015	CNRS–PAN 🇫🇷 🇵🇱	BehaPPi-BMC Behavior preserving parametric bounded model checking	co-porteur	4	8k€
2014	BQR 🇫🇷	SynPaTiC Synthèse de paramètres temporels distribuée et multi-cœurs	Porteur	2	15k€
2013	Actions émergentes GDR GPL 🇫🇷	IOP Intégration d’outils à la plate-forme CosyVerif	Porteur	1	2k€
2012–2014	PHC Merlion 🇫🇷 🇸🇬	BRAVOS Software Verification from Design to Implementation	co-porteur	6	30k€

Participant à des projets

Année	Appel	Nom du projet	Porteur	Membres	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€

Comités de programme et évaluations

Comités de programme

2025

🇺🇸HSCC 2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

Comités de pilotage

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

Organisation de congrès

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)

Rapporteur de thèses de doctorat

Année	Doctorant⋅e	Institution
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, Singapour 🇸🇬
2019	Du Xiaoning	Nanyang Technological University, Singapour 🇸🇬
2018	Wang Junjie	Nanyang Technological University, Singapour 🇸🇬
2018	Chandramohan Mahinthan	Nanyang Technological University, Singapour 🇸🇬
2017	Wu Zhimin	Nanyang Technological University, Singapour 🇸🇬
2013	Zhu Huiquan	Université Nationale de Singapour 🇸🇬

Expert scientifique

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

Développement logicel

IMITATOR : synthèse de paramètres pour les systèmes temps-réel

J’ai créé l’outil IMITATOR en 2008, et suis depuis son principal développeur.

IMITATOR est un logiciel pour synthétiser des valeurs de paramètres temporels dans les systèmes temporisés concurrents modélisés par des extensions des automates temporisés paramétrés.

IMITATOR a été utilisé dans le cadre de plusieurs collaborations avec l’industrie, notamment pour la vérification de systèmes matériels et pour l’analyse d’ordonnancement en présence d’incertitude.

Un langage d’entrée expressif

IMITATOR effectue de la synthèse de paramètres pour les systèmes temps-réel modélisés par une extension des automates temporisés paramétrés.

Des analyses puissantes

Plusieurs algorithmes sont implémentés dans IMITATOR, dont la synthèse pour la sûreté, l’absence de deadlocks, le model-checking paramétré non-Zeno, ou encore l’analyse de robustesse.

Sorties graphiques

En plus des sorties normalisées, IMITATOR génère des sorties graphiques tells que les zones de bon fonctionnement des paramètres temporels.

Un logiciel libre

IMITATOR est entièrement libre et est distribué selon les termes de la licence publique générale GNU.

Plus sur IMITATOR…

Autres outils logiciels

PAT

Membre de l’équipe de développement (2010-2013)

PAT est un model-checker puissant pour de multiples formalismes, dont timed CSP, les systèmes probabilistes, les systèmes paramétrés… PAT est principalement développé à Singapour (NUS, STUD, NTU).

PolyOp

Développeur

PolyOp est une interface simple pour encapsuler des opérations sur les polyèdres fournies par la bibliothèque PPL (Parma Polyhedra Library).

PSyHCoS

Développeur

PSyHCoS est un outil de synthèse de paramètres pour l’algèbre de processus Parametric Stateful Timed CSP (PSTCSP).

HyMITATOR

Développeur

HyMITATOR est une variante d’IMITATOR pour les automates hybrides paramétrés.

InSPEQTor

Développeur

InSPEQTor est une implémentation de la méthode inverse pour les graphes orientés valués paramétrés.

ImpRator

Développeur

ImpRator est une implémentation de la méthode inverse pour les processus de décision markoviens paramétrés.

Étudiant⋅e⋅s

Doctorants

Sarah Dépernet

(2024-…)

Vérification de propriétés de cybersécurité à l’aide de méthodes formelles
Co-encadrement avec Engel Lefaucheux

Dylan Marinho

(2020-2023)

Détection d’attaques temporisées à l’aide de méthodes formelles

Jawher Jerray

(2018-2021)

Analyses formelles de systèmes temps-réel
Co-encadrement avec Laurent Fribourg

Mathias Ramparison

(2016-2019)

Vérification de systèmes temps-réel paramétrés avec préemption
Co-encadrement avec Didier Lime
Situation actuelle : maître de conférences à Verimag

Nguyễn Hoàng Gia

(2015-2018)

Synthèse de paramètres efficace et distribuée pour les automates temporisés paramétrés
Co-encadrement avec Laure Petrucci
Situation actuelle : Post-doc au CEA (France)

Mohamed Mahdi Benmoussa

(2013-2016)

Spécification avec UML
Co-encadrement avec Christine Choppy
Situation actuelle : maître de conférences à l’École Nationale Polytechnique de Constantine (Algérie)

Romain Soulat

(2010-2013)

Synthèse d’ordonnanceurs corrects par construction pour les systèmes hybrides
Co-encadrement avec Laurent Fribourg
Situation actuelle : Technical Lead for Certification, Input Output

Post-docs

Emily Clement (2024-…)

Monitoring de systèmes cyber-physiques

Laetitia Laversa (2023-2024)

Contrôle de l’opacité dans les systèmes temporisés
Co-encadrement avec Marie Duflot, Engel Lefaucheux

Johan Arcile (2020-2022)

Détection de failles temporelles avec des méthodes formelles
Situation actuelle : maître de conférences à l’Université Paris-Saclay

Étudiant⋅e⋅s de master

Nom	Année
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

Parcours universitaire

Professeur à l’Université de Lorraine

J’ai été de 2019 à 2022 professeur des universités à l’Université de Lorraine : enseignement à l’IUT Charlemagne et recherche dans l’équipe VeriDis du LORIA.

Maîtrise de conférences

J’ai été de 2011 à 2019 maître de conférences dans l’équipe LoVe du Laboratoire d’informatique de Paris Nord à l’Université Sorbonne Paris Nord (ex-Paris 13).

Post-doctorat

J’ai effectué de décembre 2010 à août 2011 un post-doctorat au sein de l’équipe du professeur Dong Jin Song (董劲松) à l’Université Nationale de Singapour.
Je maintiens des collaborations avec plusieurs chercheurs singapouriens.