Nathalie Bertrand's homepage

Inria Researcher

Head of SUMO team of Inria Rennes Bretagne-Atlantique research center and IRISA lab
Co-head (with Pierre-Alain Reynier) of the working group on Verification of the GDR IM of the CNRS

Research topics Formal methods, Verification, Model checking, Probabilistic systems, Automata, Games
Brief bio PhD from ENS Cachan in October 2006, 1-year post-doc at TU Dresden, hired Inria researcher in October 2007, Habilitation (HDR) from University Rennes 1 in November 2015
CV version from Sept 2021

Contact information

Mail nathalie.bertrand@inria.fr
Address Inria Rennes Bretagne-Atlantique
Campus Universitaire de Beaulieu
35042 Rennes cedex - France
Tel. +33 (0)2 99 84 22 81
Fax +33 (0)2 99 84 71 71

Events

FoSSaCS'21
(online, Mar 2021)
PC member

ICALP'21
(online, July 2021)
PC member

OPODIS'21
(Strasbourg, Dec 2021)
Invited speaker

FoSSaCS'22
(Munich, Apr 2022)
Invited speaker

Concur'22
(Warsaw, Sept 2022)
PC member

Formats'22
(Warsaw, Sept 2022)
PC member

FoSSaCS'23
(Paris, April 2023)
PC member

News

Accepted paper at DISC'22

Accepted brief announcement at PODC'22

Accepted paper at ICALP'22

Suman Sadhukhan defended his PhD thesis. Congrats!

Invited speaker at GDR-IM National days in March 2022

Welcome to Nicolas Waldburger, who starts his PhD under our joint supervision with Nicolas Markey and Ocan Sankur.

Anirban Majumdar defended his PhD thesis. Congrats!

Interview of Ahmed Bouajjani and Javier Esparza for their Concur Test-of-Time award 2021

Invited speaker at FoSSaCS'22

Joining the editorial board of JLAMP

Two accepted papers at Concur'21

Invited speaker at OPODIS'21

Accepted paper at VMCAI'21

Two accepted papers at FSTTCS'20

Invited speaker at MFCS'20

Inviter speaker at DisCoTec'20

PC member of ICALP'21

Paper in SIGLOG verification column

PC member of FoSSaCS'21

Recent work

[PODC 2022] Holistic Verification of Blockchain Consensus (brief announcement), joint work with Vincent Gramoli, Marijana Lazic, Igor Konnov, Pierre Tholoniat and Josef Widder

[ICALP 2022] Parameterized safety verification of round-based shared-memory systems, joint work with Nicolas Markey, Ocan Sankur and Nicolas Waldburger

[Concur 2021] Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms, joint work with Bastien Thomas and Josef Widder

[Concur 2021] Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking, joint work with Jakob Piribauer (first author), Christel Baier and Ocan Sankur

[LMCS 2021] Reconfiguration and Message Losses in Parameterized Broadcast Networks, joint work with Patricia Bouyer and Anirban Majumdar

[VMCAI 2021] A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries, joint work with Marijana Lazic and Josef Widder

[DEDS 2020] Diagnosis and Degradation Control for Probabilistic Systems, joint work with Serge Haddad and Engel Lefaucheux

[FSTTCS 2020] Synthesizing safe coalition strategies, joint work with Patricia Bouyer and Anirban Majumdar

[FSTTCS 2020] Dynamic Network Congestion Games, joint work with Nicolas Markey, Suman Sadhukhan and Ocan Sankur

[MFCS 2020] Concurrent Games with Arbitrarily Many Players (invited paper)

[SigLog News] Model checking randomized distributed algorithms

Students

Current PhD candidates

Nicolas Waldburger, Parameterized verification of distributed algorithms under fairness conditions, with Nicolas Markey and Ocan Sankur (2021-2024)

Bastien Thomas, Automated verification of randomised distributed algorithms, with Josef Widder (2019-2022)

Previous PhD students

Suman Sadhukhan, A verification perspective to congestion games, with Nicolas Markey and Ocan Sankur (2018-2021)

Anirban Majumdar, Verification and Synthesis of Parameterized Concurrent Systems, with Patricia Bouyer (2018-2021)

Engel Lefaucheux, Controlling information in stochastic systems, with Serge Haddad (2015-2018)

Paulin Fournier, Parameterized verification of probabilistic systems, with Thierry Jéron (2012-2015)

Amélie Stainer, Quantitative verification of timed automata, with Thierry Jéron (2010-2013)

Projects

QuantProb Inria Associated team with TU Dresden: Quantitative analysis of non-standard properties for probabilistic models (2016-2018)
STOCH-MC Stochastic Models: Scalable Model Checking (2014-2018)
AVerTS Algorithmic Verification of Real-Time Systems (2014-2016)
DISTOL DIStributed and STOchastic systems, Logic (2013-2015)
ImpRo Implementability and Robustness of Timed Systems (2011-2014)
VACSIM Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle (2012-2015)
STP Tournesol project on Probabilistic Timed Systems (2009-2011)
PIPS Procope project on Partial Information Probabilistic Systems (2008-2010)
TESTEC TEst des Systèmes Temps réel Embarqués Critiques (2008-2011)
COMBEST COMponent-Based Embedded Systems design Techniques (2008-2011)
ACI Persée (2003-2006)
VOSS II (2006-2007)

Academic duties

Editorial board member of JLAMP
Program committee member of: STACS'16, TACAS'16, Concur'16, QEST'16, LICS'17, FCT'17, MSR'17, FoSSaCS'18, ICALP'18, MFCS'19, RP'19, TIME'19, FORTE'20, FoSSaCS'21, ICALP'21, Concur'22 and more in the previous years.
Co-chair of Formats'20 program commitee. Previously co-chair of QEST'17, QAPL'14, and QAPL'15 program committees.

Nominated member (2016-2019) of the CNU 27: Conseil National des Universités, section 27.
Member (2012-2015) and scientific secretary (2013-2015) of Gilles Kahn PhD award committee.
Member of the steering committee of QEST (2012-2015).