

2 au 4 novembre 2026
IRISA et Inria, Université de Rennes
The GT VERIF annual meeting 2026 will take place on November 2–4 in Rennes at IRISA/Inria. It will span four half-days, from the afternoon of the 2nd to the morning of the 4th.
The meeting aims to bring together the French community in formal verification—particularly junior researchers, doctoral students, and postdocs—with the goal of fostering collaboration and openness to topics related to verification.
However, colleagues from other countries are very welcome! Please note that most talks will be in English.
The event aims to cover all areas of formal verification, including (among others!):
- formal verification of computer systems
- the use of automated or interactive proof techniques (model checking, automated deduction, proof assistants, SMT solvers, etc., as well as combinations thereof),
- the use of logics to reason about system properties (e.g., temporal, spatial, probabilistic, or data-driven logics),
- abstraction techniques for verification.
Call for Talks / Registration
Registration is free but mandatory before October 22, 2026:
Register here!
Registration includes the lunch on November 3 and coffee breaks.
Important Dates
- Dates of the meeting: November, 2-4, 2026
Deadline for talk proposals : 19/10/2026
(the schedule for participant talks is full)- Registration deadline : 22/10/2026
Programme
Invited Talks :
- Julien Brunel (ONERA)
Alloy and Formal Verification of Distributed Systems - Augustin Lemesle (CEA, List)
Formal trustworthiness of AI: tooling the methods - Sylvain Conchon (CNRS, LMF)
TBA - Corto Mascle (MPI-SWS)
A history of population control problems - Munyque Mittelmann (CNRS, LIPN)
Strategic Reasoning in Dynamic Multi-Agent Systems - Igor Walukiewicz (CNRS, LaBRI)
Revisiting Partial-Order Reduction - Jean-Marc Talbot (Université de Bordeaux)
Session carrière (Qualification, postes de maîtres de conférences)
Schedule
Upon entering the IRISA/Inria building, turn right. You will see the entrance of the amphitheater behind a glass door.
We will be there from 1.30pm to welcome you, and give you your badge.
Monday, November 2
| 14h | Sylvain Conchon (CNRS, LMF) |
| 15 | short break |
| 15h15 | Augustin Lemesle (CEA, List) – Formal trustworthiness of AI: tooling the methods |
| 16h15 | ☕ |
| 16h45 | Carlos Olarte – Strategic and Symbolic Methods for Real-Time Systems in Maude |
| 17h05 | Laetitia Laversa – From Meta-Strategies to Timed Controllers: Control Synthesis for Execution-Time Opacity |
| 17h25 | Maëlle Gautrin – Reaching as cheap as possible in robust weighted timed games |
| 17h45 | Rémi Parrot – Active learning of Petri Net with sledge languages (Work-In-Progress) |
| 18h05 | Loïc Hélouët -Values and Strategies in Regular MDPs |
Tuesday, November 3
| 9h | Julien Brunel (ONERA) – Alloy and Formal Verification of Distributed Systems |
| 10 | ☕ |
| 10h30 | Corentin Barloy – Shuffles of Context-Free Languages Along Regular Trajectories |
| 10h50 | Keya Prakash – On the parity index hierarchy problem |
| 11h10 | Luc Lapointe – WinPop: A decidable tiling problem |
| 11h30 | Christophe Grandmont – On Automata-Based Preferences in Games Played on Graphs |
| 11h50 | Gaëtan Staquet – Antichains for Concurrent Parametric Games |
| 12h10 | 🍴 |
| 14h | Corto Mascle (MPI-SWS) – A history of population control problems |
| 15h | short break |
| 15h15 | Munyque Mittelmann (CNRS, LIPN) – Strategic Reasoning in Dynamic Multi-Agent Systems |
| 16h15 | ☕ |
| 16h45 | Open Problems Session |
Wednesday, November 4
| 9h | Igor Walukiewicz (CNRS, LaBRI) – Revisiting Partial-Order Reduction |
| 10 | ☕ |
| 10h30 | Jean-Marc Talbot (Université de Bordeaux). Session carrière (en français) |
| 11h30 | James C. A. Main – Perturbation equivalence in labelled Markov chains |
| 11h50 | Isa Vialard – Approximating the value of time-bounded weighted timed games |
Organization
- Tali Sznajder (LIP6, Sorbonne Université)
- Ocan Sankur (IRISA, CNRS)
- Laurence Dinh (Inria)
(avec l’aimable concours du Centre Inria de l’Université de
Rennes)