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.

"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

Formal Verification of Adaptive Control Algorithms (2023-2026, CEFIPRA)

Collaboration IIT Bangalore and IIT Goa (India) on the verification of control algorithms that evolve according to their environment.

ROBSYS - Robustesse des systèmes autonomes (2023-2026)

The MTV team is involved in the first work package on "formal specification and runtime model checking for task planning embedded software, or e.g. ROS (Robot Operating System)-based system"

Tools

ARC

A model-checking tool for the AltaRica language.

DeepSynth

Learning techniques for program synthesis.

TaPAS

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

TChecker

An extensible model-checker for real-time systems.

The CoLoMoTo Interactive Notebook

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

Pint

Static analyzer for reachability in discrete automata networks.

Members

Clotilde Bizière

PhD student

Déborah Boyenval

Postdoc

Frédérique Carrère

MC U. Bordeaux

Théo De Castro Pinto

PhD student

Romain Delpy

PhD student

Nathanaël Fijalkow

CR CNRS

Emmanuel Fleury

MC U. Bordeaux

Hugo Gimbert

CR CNRS

Charles Grellois

MC Bordeaux INP

Alain Griffault

MC U. Bordeaux

Frédéric Herbreteau

MC Bordeaux INP, head

Mathieu Hilaire

PhD student

Thibault Hilaire

PhD student

Aïda Ibrahim

PhD student

David Janin

MC (HDR) Bordeaux INP

Sarah Larroze-Jardiné

PhD student

Jérôme Leroux

DR CNRS

Corto Mascle

PhD student

Théo Matricon

PhD student

Rémi Morvan

PhD student

Mohamed Mosbah

PR Bordeaux INP

Anca Muscholl

PR U. Bordeaux

Loïc Paulevé

DR CNRS

Vincent Penelle

MC U. Bordeaux

Gérald Point

IR CNRS

Sylvain Raïs

PhD student UB/ONERA

Antoine Rollet

MC (HDR) Bordeaux INP

Grégoire Sutre

CR CNRS

Athénaïs Vaginay

Postdoc

Igor Walukiewicz

DR CNRS

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.

If you wish to give a talk or invite a speaker, please contact Clotilde Bizière, Romain Delpy or Frédéric Herbreteau.

-
05/12/2024 Tibaut Benjamin (U. Cambridge) TBA
14/11/2024 Loïc Paulevé (LaBRI) TBA
17/10/2024 Clotilde Bizière (LaBRI) TBA
26/09/2024 Aditya Prakash (U. Warwick) Recognising history-deterministic parity atutomata
27/06/2024 Romain Delpy (LaBRI) An automata based approach for synchronizable mailbox communication
13/06/2024 Sougata Bose (U. Liverpool) Solving Concurrent Mean-payoff games with Bounded-memory Strategies
28/05/2024 Léo Exibard (U. Gustave Eiffel) Runtime monitoring for Hennessy-Milner logic with recursion over systems with data
16/05/2024 Corto Mascle (LaBRI) Minimising (history-)deterministic generalised (co-)Büchi automata
28/03/2024 Balasubramanian Ayikudi (MPI-SWS) Reachability in Continuous Pushdown VASS
21/03/2024 Mathieu Hilaire (U. Clermont-Ferrand) Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete
19/03/2024 Julie Parreaux (U. Warsaw) Weighted Timed Games: Decidability, Randomness and Robustness
14/03/2024 Thibault Hilaire (LaBRI) A State-of-the-Art Karp-Miller Algorithm Certified in Coq
15/02/2024 Philipp Czerner (TUM) Making IP = PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms
01/02/2024 Ocan Sankur (IRISA) Timed Automata Verification and Synthesis via Finite Automata Learning
18/01/2024 B Srivathsan (CMI, Chennai) Deterministic Suffix-reading Automata
07/12/2023 Thejaswini (U. Warwick) Solving parity and Rabin games using attractor decompositions
27/11/2023 Alexis Reynouard (ULB) Implementing the Surprise Effect in Timed Games
23/11/2023 Antonio Casares (LaBRI) PhD defense "Propriétés structurelles des automates sur les mots infinis et mémoire pour les jeux" (starts at 13:30!!!)
09/11/2023 Déborah Boyenval (U. Côte d'Azur) Formal modeling of the discrete dynamics of intrinsic cell cycle checkpoints: a proof of concept
19/10/2023 Nicola Gigante (Free University of Bozen-Bolzano) Temporal Logics Modulo Theories for Infinite-State Verification
28/09/2023 Loïc Paulevé (LaBRI) Tackling Universal Properties of Minimal Trap Spaces of Boolean Networks
14/09/2023 Jérôme Leroux (LaBRI) The Semilinear Home-Space Problem is Ackermann-Complete for Petri Nets
22/06/2023 Dylan Marinho (LORIA) Ensuring opacity in timed systems
08/06/2023 Corto Mascle (LaBRI) Parameterized Broadcast Networks with Registers
25/05/2023 Chana Weil-Kennedy (IMDEA) Observation Petri Nets
13/04/2023 Théo Matricon (LaBRI) Language Sharpening for Program Synthesis
02/03/2023 Pierre Vandenhove (U. Mons) Memory Requirements of Omega-Regular Objectives: the Regular Case
26/01/2023 Celia Biane (IRISA) Réseaux biologiques : des systèmes dynamiques Booléens à la neuroscience expérimentale
12/01/2023 Mikhail Raskin (LaBRI) Getting readable proofs for replicated systems from automated provers
15/12/2022 Group discussion ChatGPT, proof and reasoning
01/12/2022 Léon Bohm Learning algorithms for ω-automata
17/11/2022 Group meeting
28/10/2022 Jérôme Leroux (LaBRI) State Complexity of Protocols with Leaders
22/09/2022 Sara Riva (U. Côte d'Azur) Hypotheses and Equations on Discrete Dynamical Systems
08/09/2022 Srivathsan B (CMI Chennai) Simulations for event-clock automata
07/07/2022 Nicolas Amat (IRIT) What is Polyhedral Reduction? ... and how we use it to accelerate the verification of reachability problems.
30/06/2022 Pierre Civit (LIP6) Dynamic Probabilistic Automata
16/06/2022 Emmanuelle Saillard (INRIA Bordeaux) PARCOACH, a tool that combines static and dynamic analyses to detect misuse of MPI communications
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
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