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

Parameterized Verification of Disjunctive Timed Networks

Latest publication

Étienne André, Paul Eichler, Swen Jacobs and Shyam Karra. Parameterized Verification of Disjunctive Timed Networks . In Rayna Dimitrova and Ori Lahav (eds.), VMCAI’24, Springer LNCS 14499, pages 124-146, January 2024. Acceptance rate: 41%. DOI: 10.1007/978-3-031-50524-9_6 (English) [BibTeX]

Research projects

Project PI

Year Call Project name Role Permanent staff Budget
2020–2023
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 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€

Project participant

Year Call Project name PI Permanent staff Budget
2023–2027 ANR
🇫🇷
BisoUS Didier Lime 500k€
2018–2019 ERATO
🇯🇵
MMSD
Metamathematics for Systems Design
Ichiro Hasuo (蓮尾 一郎) > 20 10000k€
2019–2020
ongoing
PICS
🇫🇷 🇵🇱
PARTIES
verification of PARametric TIme constrained strategic abilitiES for agents acting under incomplete information
Laure Petrucci 7 8k€
2018–2019
ongoing
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

2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013

Steering committees

Conference organization

PhD theses reviewer

Scientific expert

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

PhD students

Dylan Marinho

(2020-2023)

Dylan Marinho Detecting timed attacks using formal methods

Jawher Jerray

(2018-2021)

Jawher Jerray Formal analyses of real-time systems
Co-supervised by Laurent Fribourg

Mathias Ramparison

(2016-2019)

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

Nguyễn Hoàng Gia

(2015-2018)

Nguyễn Hoàng Gia 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)

Mahdi Benmoussa Specification with the UML
Co-supervised by Christine Choppy
Current situation: Associate 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)

Post-docs

Laetitia Laversa (2023-…)

Johan Arcile (2020-2022)

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

Master students

Name Year
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

Contact

Affiliation

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

Snail mail address

Étienne André
Institut Galilée
LIPN
Université Sorbonne Paris Nord
93430 Villetaneuse
France

E-Mail address

Etienne.Andre(at)lipn.fr

Phone

Please send me an email first

Fax

…in 2024…? like seriously…?

ha-index

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