Research interests

Current research projects

BNeDiction (2021-2025, funded by ANR)

The project aims at providing a general methodology for making predictions from data on systems structure and dynamics by the means of ensembles of Boolean networks.

InDID (2019-2023, funded by Connecting Europe Facility)

Develop a digital infrastructure for intelligent transport systems and autonomous transportation.

"Vers des réseaux véhiculaires 5G" (2019-2022, funded by Région Nouvelle-Aquitaine)

TickTac (2019-2023, funded by ANR)

Efficient Techniques and Tools for the Verification and Synthesis of Real-Time Systems.

Codys (2018-2022, funded by ANR)

Orbites des systèmes dynamiques discrets en informatique.

DeepSynth (2019-2021, funded by CNRS Momentum)

Learning techniques for program synthesis.

ESTATE (2016-2021, funded by ANR)

Lay the foundations of a new algorithmic framework for enabling Autonomic Computing in distributed and highly dynamic systems and networks.

"De la loi au code" (funded by CNRS Prime project and MESRI)

Spécification et vérification des algorithmes de décision publique pour établir la concordance entre le code et la loi

BraVAS (2017-2022, funded by ANR)

Ideal-based algorithms for VASSes and well-structured systems



A model-checking tool for the AltaRica language.


A set of ANSI C libraries related to Presburger Arithmetic and a small solver program.


An extensible model-checker for real-time systems.

The CoLoMoTo Interactive Notebook

Accessible and reproducible computational analyses of qualitative models of biological networks.


Static analyzer for reachability in discrete automata networks.


Pierre Castéran

MC U. Bordeaux

Frédérique Carrère

MC U. Bordeaux

Antonio Casares-Santos

PhD student

Theo De Castro Pinto

PhD student

Patrick Félix

MC U. Bordeaux

Nathanaël Fijalkow


Emmanuel Fleury

MC U. Bordeaux

Hugo Gimbert


Alain Griffault

MC U. Bordeaux

Frédéric Herbreteau

MC Bordeaux INP, head

Thibault Hilaire

PhD student

Aïda Ibrahim

PhD student

David Janin

MC (HDR) Bordeaux INP

Sarah Larroze-Jardiné

PhD student

Jérôme Leroux


Corto Mascle

PhD student

Rémi Morvan

PhD student

Mohamed Mosbah

PR Bordeaux INP

Anca Muscholl

PR U. Bordeaux

Loïc Paulevé


Vincent Penelle

MC U. Bordeaux

Gérald Point


Adrien Prévost

PhD student U. Bordeaux/SNCF

Antoine Rollet

MC (HDR) Bordeaux INP

Grégoire Sutre


Igor Walukiewicz


Pascal Weil


Marc Zeitoun

PR U. Bordeaux

Group meetings

The MTV group meeting happens at 13:00. Please, refer to the shared calendar for the meeting room. Most group meetings can be attended online on Zoom.

30/06/2022 Pierre Civit (LIP6) TBA
16/06/2022 Emmanuelle Saillard (INRIA Bordeaux) TBA
02/06/2022 Frédéric Herbreteau (LaBRI) Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
07/04/2022 Samuel Pastva (U Brno) Finding SCCs in many systems at once using symbolic algorithms
10/03/2022 Hugo Gimbert (LaBRI) Distributed Asynchronous Games With Causal Memory are Undecidable
17/02/2022 Abdelhakim Baouya (Verimag) Artificial Intelligence meets Formal Methods: Generation and verification of learned stochastic automata
14/02/2022 Charles Grellois (LIS) Verification of (probabilistic) functional programs
03/02/2022 Damien Busatto-Gaston (ULB) On the strategy synthesis problem in MDPs: probabilistic CTL and rolling windows
06/01/2022 Laure Petrucci (LIPN) Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata
09/12/2021 Benedikt Bollig (LMF) Synthesis in Presence of Dynamic Links
25/11/2021 Benoît Delahaye (LS2N) Vérification formelle et statistique de modèles paramétriques
28/10/2021 Corto Mascle (LaBRI) Responsibility and verification: Importance value in temporal logics
14/10/2021 Nathanaël Fijalkow (LaBRI) Learning LTL formulas
30/09/2021 at 14:00!!! Anirban Majumdar (LMF) PhD defense "Verification and Synthesis of Parameterized Concurrent Systems" (see framacal for visio info)
01/07/2021 Arnaud Sangnier (IRIF) Reachability in Distributed Memory Automata
24/06/2021 Aïda Ibrahim (LaBRI) spécification et la vérification du code informatique de Tachygraphe
17/06/2021 Igor Khmelnitsky (LMF) Minimal coverability tree construction made complete and efficient
03/06/2021 Salomon Sickert-Zehnter (TUM) Practical synthesis of reactive systems from LTL specifications
29/04/2021 Jérôme Leroux (LaBRI) Flat Petri Nets
11/03/2021 Loïc Paulevé (LaBRI) Semantics, verification, synthesis and control of Boolean automata networks
25/02/2021 Igor Walukiewicz (LaBRI) Partial-order reductions
© MTV, Design: HTML5 UP