Nathalie Bertrand's homepage

Inria Researcher

Head of DEVINE team of Inria Centre at Rennes University and IRISA lab
Co-head (with Pierre-Alain Reynier) of the working group on Verification of the GDR IFM of the CNRS
Active member of the gender equality commission of IRISA and Inria Rennes, and Inria committee on gender equality and equal opportunity.

Research topics Formal methods, Verification, Model checking, Parameterized systems, Quantitative models, 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

NETYS'23
(Benguerir, May 2023)
PC member

VMCAI'24
(London, Jan 2024)
PC member

MOVEP'24
(Rennes, May 2024)
co-organiser

FoSSaCS'25
(Hamilton, May 2025)
PC member

MFCS'25
(Warsaw, August 2025)
PC member

News

Our new research team DEVINE has been created on Jan 1st 2024. The website is up and running!

With Nicolas Markey we are organizing the verification summer school MOVEP'24 from May 27th to May 31st in Rennes. Spread the news and encourage your students to attend!

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

Luc Lapointe, Games with arbitrary many players, with Patricia Bouyer-Decitre (2023-)

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

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

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

PAVEDYS (2024-2028)
BisoUS (2023-2026)
MAVeriQ (2020-2024)

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 and TCS
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, VMCAI 2024, FoSSaCS'25 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).