Pierre-Alain Reynier

Professor, Aix-Marseille University, Computer Science department

Researcher at LIS

Head of the modelisation and verification (MoVe) group at LIS

Head of the Master Curriculum "Parcours Informatique et Mathématiques Discrètes" (Computer Science and Discrete Maths)

Co-head (with Nathalie Bertrand) of the working group on Verification of the GDR IM of the CNRS


Laboratoire d’Informatique et Systèmes
Parc Scientifique de Luminy
163 avenue de Luminy - Case 901
F-13288 Marseille Cedex 9, France

Office : A208 (academic library, 2nd floor)
Phone : +33 (0)4 86 09 06 73
Fax : +33 (0)4 86 09 ?? ??

E-mail : firstname.lastname@lis-lab.fr (New!)



I am a member of the Program Committee of the 40th International Conference on Applications and Theory of Petri Nets and Concurrency (Petri Nets 2019).

I am a member of the Program Committee of the Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019).

Nouvelle formation de master 2018/2022 (new training offer): Parcours Informatique et Mathématiques Discrètes (Computer Science and Discrete Maths)

The 12th edition of the international Conference on Reachability Problems (RP 2018) will be held in Marseille on 24-26 September 2018.

The next edition of the annual meeting of GT-Verif will be held in Grenoble, organized by Radu Iosif at Verimag, on 28-30 May 2018.

Forthcoming talk at National Days of GDR-IM on April 4th.

Recent talk on Feb. 22nd at Oxford CS department on register minimization for SST: slides

I am a member of the Program Committee of the 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018).

Our algorithm Monotone Pruning for the computation of the minimal coverability set of Petri nets has been implemented in C++ by Florent Jaillet. The tool can be found there.

The french colloquium on Modelization of Reactive Systems (MSR) was held in Marseille in 2017. Please visit the webpage.

Recent work:

Research Topics:

Formal Methods, Verification, Model-Checking, Automata, Logic, Transducers, Timed systems, Petri nets, Concurrency, Robustness.

More details are available via the Research link.

Curriculum Vitae:

A version can be found here (updated nov. 2017).


They are available via the Publications link.


Informations (in french) are available via the Teaching link.