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
Jérôme LEROUX

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:
Publications


Students

Ph.D. proposals Ph.D students and postdocs
Miscs