An expressive input language
IMITATOR performs parameter synthesis for real-time systems modeled by an extension of parametric timed automata.
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.
Masaki Waga (和賀 正樹) and Étienne André. Hyper parametric timed CTL. In Alessandro Biondi and Martina Maggio (eds.), EMSOFT’24, ACM/IEEE, September 2024. To appear. (English)
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€ |
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€ |
Year | Phd student | Institution |
---|---|---|
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 🇸🇬 |
Year | Institution | |
---|---|---|
2020 | 🇯🇵 | EIG CONCERT-Japan |
2015, 2016 | 🇫🇷 | Agence nationale de la recherche |
2014 | 🇳🇱 | Nederlandse Organisatie voor Wetenschappelijk Onderzoek |
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.
IMITATOR performs parameter synthesis for real-time systems modeled by an extension of parametric timed automata.
Various algorithms are implemented in IMITATOR, including safety parameter synthesis, deadlock-freeness, non-Zeno parametric model-checking or robustness analysis.
In addition to results output using predefined formats, IMITATOR generates graphical outputs such as the zones of good behaviors for the timing parameters.
IMITATOR is entirely open-source and is distributed under the GNU General Public License.
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).
HyMITATOR is a fork of IMITATOR for parametric hybrid automata.
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.
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 |
I have been from 2019 to 2022 full professor with Université de Lorraine, member of the VeriDis research team of LORIA.
I have been from 2011 to 2019 an associate professor in the LoVe team of LIPN with Université Sorbonne Paris Nord (formerly "Paris 13").
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.
I wrote my Ph.D. thesis from September 2007 to December 2010 in the Laboratoire Spécification et Vérification, ENS Cachan, France of the École Normale Supérieure de Cachan, France under the supervision of Laurent Fribourg and Emmanuelle Encrenaz.
Title: An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems [PDF ].
I maintain a list of conferences in formal methods.
Université Sorbonne Paris Nord, LIPN, CNRS UMR 7030, F-93430 Villetaneuse, France
Étienne André
Institut Galilée
LIPN
Université Sorbonne Paris Nord
93430 Villetaneuse
France
Etienne.Andre(at)lipn.fr
Please send me an email first
…in 2024…? like seriously…?
I am very proud that my ha-index is 78.