CNRS-LABRI-MVTSI : Jérôme LEROUX

Jérôme LEROUX
DR CNRS

Laboratoire Bordelais de Recherche en Informatique (LaBRI)
Equipe Méthodes Formelles (MF)
Domaine Universitaire
351 cours de la liberation
33405 Talence Cedex
FRANCE

Phone :	+33 54000 3509
Fax :	+33 54000 6669
E-Mail :	jerome DOT leroux AT labri DOT fr
Office :	264

Research Interests

The Vector Addition System Reachability Problem
Petri Nets is one of the most popular formal models for the representation and the analysis of parallel processes. The reachability problem is central since many computational problems (even outside the realm of parallel processes) reduce to this problem. The reachability problem is difficult and its decidability remained open during 20 years.

Arithmetic automata and Presburger arithmetic
Finite state automata provide a simple way for deciding the satisfiability of a Presburger formula. Since 1962 we know that for the positional notation of natural numbers and vectors of natural numbers, the solutions of Presburger formulas are encoded by regular languages that can be effectively represented by finite state automata. Related tools:

Talence Presburger Arithmetic Suite

Publications

Students

Ph.D. proposals

Ph.D students and postdocs

Alexander Heußner (Ph.D. Bordeaux 1, 2011): Towards the verfication of safety properties for communicating infinite systems: decidability and abstraction refinement.
M. Praveen (Postdoc, 2013): Boundedness Problem for Pushdown Vector Addition Systems.
Patrick Totzke (Postdoc, 2014): Pushdown Vector Addition Systems in small dimensions.
Thomas Geffroy (Ph.D. Bordeaux 2014-2017): High Quality Abstractions For The Verification Of Asynchronous Distributed Systems.
Thibault Hilaire (Ph.D. student Bordeaux, 2021-2024): Certification in Coq of Distributed Systems.

Miscs

Steering committee of "Conferences on Reachability Problems" RP /
Co-organizer or organizer of MFCS'23 GT VERIF'22, GandALF'19. JM'18, RP'12,
Program committees chair or co-chair of MFCS'23, GandALF'19, RP'12.
Program committees of RP'24, RP'23, RP'22, ICALP'22, LICS'21, GandALF'20, GandALF'18, CONCUR'18, JM'18, CONCUR'17, RP'17, FCT'17, CONCUR'16, STACS'15, HIGHLIGHT'14, RP'13, MSR'13, AISS'12, INFINITY'11, ATVA'11, MSR'11, RP'11, INFINITY'09.
Invited talks/tutorials at FoSSaCS'24 PETRI NETS'21, DNA'20, LICS - ICALP'20, HIGHLIGHTS'19, MFCS'19, CAAL'19, JN IM'19, INFINITY'18, STACS'16, RP'15, ATVA'13, VPT'13, LATA'11, PAVAS(2011), Automata and Logic (2011), MOVEP'10
I used to be a co-organizer of the MVTSI Seminar. See MF Seminar for recent and upcoming seminars in our team.
PHD's jury member of Matthieu Renard (2017 - Université de Bordeaux. Directed by Antoine Rollet, Mohamed Mosbah, and Yliès Falcone), Nicolas David (2017 - Université de Nantes. Directed by Claud Jard and Didier Lime), Arthur Michior (2016 - University Paris-6. Directed by Olivier Carton and Alexis Bès), Michael Blondin (2016 - ENS-Cachan. Directed by Alain Finkel and Pierre McKenzie), Julien Reichert (2015 - ENS-Cachan. Directed by Dietmar Berwanger and Laurent Doyen), Paulin Fournier (2015 - IRISA. Directed by Nathalie Bertrand and Thierry Jéron), Sylvain Salvati (2015 - LaBRI. HDR), Victor Marsault (2015 - Telecom ParisTech. Directed by Jacques Sakarovitch), Vincent Penelle (2015 - University Paris Est. Directed by Antoine Meyer and Didier Caucal), Florent Avellaneda (2013 - University of Marseille. Directed by Peter Niebert), Jean-François Degbomont (2013 - University of Liège. Directed by Bernard Boigelot), Peter Schrammel (2012 - University of Grenoble. Directed by Alain Girault and Bertrand Jeannet), Assalé Adjé (2011 - X. Directed by Stéphane Gaubert et Éric Goubault), Julien Brusten (2011 - University of Liège. Directed by Bernard Boigelot), and Florent Bouchy (2009 - LSV. Directed by Alain Finkel).
Best paper award at TURING'100