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.
Research interests
- Foundations of formal verification and controller synthesis
- Modelling, synthesis and verification of communicating, concurrent and distributed systems
- Program verification and synthesis
- Dependability, software testing and runtime verification
- Software model-checking and trustworthy computing
- Quantitative modelling and verification
- Game theory for formal verification
- Formal computational methods and systems biology
- Machine learning and controller synthesis
- Automated theorem proving, proof of programs
Current research projects
"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
MC U. Bordeaux
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
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) | Control and elimination of variables in Boolean networks |
| 17/10/2024 | Clotilde Bizière (LaBRI) | Reachability in 2-dimensional Branching VASS |
| 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