Journées Annuelles 2025 — Groupe de travail GT-Vérif

Université Paris-Est — Créteil (LACL) | Du 05/11/2025 au 07/11/2025

FR

Présentation

Les journées annuelles du GT‑Vérif se tiendront du 05/11/2025 au 07/11/2025 à l'Université Paris‑Est — Créteil. Elles ont pour objectif de rassembler la communauté française travaillant en vérification formelle, en particulier les chercheurs juniors, doctorants et post‑doctorants, afin de favoriser les collaborations et l'ouverture sur des thématiques liées à la vérification.

Thématiques couvertes :

Inscription

Les inscriptions sont gratuites. Merci de vous inscrire avant le 05/11/2025.

Formulaire d’inscription : ici

Appel à exposés

Toute personne souhaitant donner un exposé lors de ces journées est invitée à l’indiquer dans le formulaire d’inscription.

Si vous souhaitez donner un exposé mais n’avez pas encore de sujet précis, vous pouvez envoyer les informations avant le 22/10/2025 par mail à copil-gt-verif@inria.fr

Programme

Le programme comprend 4 demi‑journées, du 5 après-midi au 7 au matin, avec exposés invités et présentations de jeunes chercheurs.

Orateurs invités :

Mercredi 5 novembre — Matin

Événement co-hébergé : Séminaire Paris ACTS

Mercredi 5 novembre — Après-midi

Lieu : Amphi MSE, Maison des Sciences et de l’Environnement

Horaire Intervenant Titre
13h30 – 14h00 Accueil
14h00 – 15h00 Guillermo A. Perez
Proof Over Promises: Making RL Trustworthy

Reinforcement Learning (RL) has shown great potential in many domains, yet its application in safety-critical contexts requires stronger guarantees. This talk explores how formal verification can enhance the reliability of learning-based systems.

15h15 – 16h15 Thom Badings
(titre à préciser)

TBA.


16h45 – 17h10 Tanguy Dubois
Statistical Model Checking of Stochastic Timed-Arc Petri Nets

Timed-Arc Petri nets (TAPN) are a timed extension of Petri nets where tokens have their age and each arc is associated with a time interval restricting the ages of tokens available for transition firing. Additionally, a TAPN can also contain place invariants constraining the ages of tokens in places, inhibitor arcs preventing a transition from firing and transport arcs that preserve a token's age upon firing. This set of features, as much as it allows us to model complex systems, also often makes verification problems computationally hard or even undecidable. Moreover, in order to model real-life examples, additional stochastic aspects are often necessary to capture the desired behaviour. We suggest (to the best of our knowledge) the first stochastic semantics for TAPNs and design and implement the Statistical Model Checking (SMC) algorithms in the model checker TAPAAL. We argue for the semantic choices we made in the stochastic semantics and prove that the semantics is well-behaving. On a number of case studies we demonstrate the practical applicability of our modelling formalism and its SMC implementation.

17h15 – 17h40 Uli Fahrenberg
Concurrent semantics of Petri nets through higher-dimensional automata

Résumé à venir.

Jeudi 6 novembre — Matin

Lieu : Amphi MSE, Maison des Sciences et de l’Environnement

Horaire Intervenant Titre
9h00 – 10h00 Frédéric Gervais
Formal specification, refinement and proof with B and Event-B

This talk is an introduction to B and Event-B formal languages, which have been created by Jean-Raymond Abrial. After a brief description of the B theory, we will focus on Event-B, the Rodin platform and the refinement and proof activities.

10h15 – 11h15 Émeric Tourniaire
System modeling and safety in railway industry

Railway systems are deemed critical in the sense that a failure can result in dramatic accidents. In this presentation we will explain how CLEARSY use formal methods and event-B to model, analyze and simulate these systems to help infrastructure managers to ensure safety on their lines.


11h45 – 12h10 Luca Paparazzo
Reachability in multi-agent transfer systems

Résumé à venir.

12h15 – 12h40 Alexandre Duret-Lutz
Engineering an LTLf synthesis tool

The problem of LTLf reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolution of the inputs and outputs has a prefix that satisfies a given LTLf specification. We describe the implementation of an LTLf synthesizer that outperforms existing tools on our benchmark suite. This is based on a new, direct translation from LTLf to a DFA represented as an array of Binary Decision Diagrams (MTBDDs) sharing their nodes. This MTBDD-based representation can be interpreted directly as a reachability game that is solved on-the-fly during its construction.

Jeudi 6 novembre — Après-midi

Lieu : Amphi MSE, Maison des Sciences et de l’Environnement

Horaire Intervenant Titre
14h00 – 15h00 Nicolas Mazzocchi
Safety and Liveness of Quantitative Properties and Automata

Safety and liveness are fundamental concepts in computer-aided verification. The safety-liveness classification of Boolean properties determines whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). This talk extends the safety-liveness framework to quantitative properties, defined as arbitrary functions from infinite words to partially ordered domains. This framework will be instantiated with the classes of quantitative properties expressed by automata, which map infinite words to real numbers. Then, procedures for deciding whether a given automaton defines a safe or live property will be presented, together with a decomposition into safe and live automata.

15h15 – 16h15 Daniela Petrisan
(titre à préciser)

Résumé à venir.


16h45 – 17h10 Sougata Bose
Memory requirements of omega-regular objectives: from deterministic to stochastic games

Stochastic zero-sum two-player games on finite graphs model reactive systems as interaction between the controller (Player 1) and the environment. The decisions of the environment are either antagonistic or stochastic, modeled by actions chosen by the opponent Player 2 or chosen randomly from a stochastic vertex. The value of a vertex is the supremum probability that Player 1 can produce a winning play starting from the vertex, no matter how the other player plays. Memory requirements for optimal strategies have been studied for both stochastic games and deterministic games (no stochastic vertices). In this work, we are interested in relating the memory requirement of stochastic games and deterministic games. For omega-regular objectives with a neutral letter, we first show that the memory requirements for winning almost-surely (with probability 1) in stochastic games is the same as in deterministic games. For strategies achieving the optimal value, we show that additional information about the Myhill-Nerode classes, that identifies the set of winning continuations, is also necessary. Conversely, we show that a product of the Myhill-Nerode automaton and the minimal memory structure for deterministic games suffices to play optimally in stochastic games. The talk is based on joint work in progress with Mickael Randour, Matéo Torrents and Pierre Vandenhove.

17h15 – 18h15 AG du GT‑Vérif

Vendredi 7 novembre — Matin

Lieu : Amphi (à préciser)

Horaire Intervenant Titre
09h00 – 10h00 Léo Henry
Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement

Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches for concurrent systems have recently emerged. This talk presents a new framework allowing to take a significant step beyond available results and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. The approach automatically refines the global alphabet into component alphabets while learning the component models. It is based on the development of a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets. This allows to characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. Based on this theory, a compositional learning algorithm implementing these ideas is presented, where learning counterexamples precisely correspond to distribution counterexamples under well-defined conditions.Finally, some experiments are presented, showing that in more than 630 subject systems, the implementation of this new algorithm delivers orders of magnitude improvements (up to five orders) in membership queries and in systems with significant concurrency, it also achieves better scalability in the number of equivalence queries.

10h15 – 10h40 Lydia Bakiri
Opacity Problems in Multi Energy Timed Automata

Résumé à venir.

10h45 – 11h10 Mouloud Amara
A Theory of (Linear-Time) Timed Monitors

Runtime Verification (RV) is gaining popularity due to its scala- bility and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula ϕ, formalising some property of interest, is typically trans- lated into a monitor that checks whether the system under scrutiny satisfies ϕ during its execution. A logical formula ϕ is violation (resp. satisfaction) moni- torable iff there exists a monitor for ϕthat is both sound and complete w.r.t. its violation (resp. satisfaction) by a system; and ϕ is monitorable if it is violation or satisfaction monitorable. The monitorability problem is thus concerned with determining the largest subset of a logic L that is monitorable. Although this problem has been solved for expressive untimed logics, it remained open for timed logics, i.e., where formulae can express both the order of events and the quantity of time separating them. In our recent work, we solved the monitorability problem for T lin , a new expressive (linear-time) timed µ-calculus that we proposed. First, we show that T lin is strictly more expressive than MTL, the de facto timed extension of the well-known LTL. Second, we identify MT lin , the largest monitorable fragment of T lin and characterise its largest subsets of formulae that are violation mon- itorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To the best of our knowledge, this is the first work that solves the monitorability problem for such an expressive timed logic. Our theoretical results are accompanied with compilers (i) from MTL to T lin and (ii) from MT lin formulae to monitors. Joint work with Giovanni Bernardi, Mohammed Foughali and Adrian Francalanza.


11h30 – 11h55 Antonio Casares
Layered automata: A canonical model of automata over infinite words

Contrary to the case of automata over finite words, omega-regular languages do not admit unique, minimal deterministic automata. Yet, not all hope is lost! In this talk I will introduce layered automata, a subclass of alternating parity automata, defined by syntactic conditions and extending deterministic ones. We show: - All layered automata are history-deterministic. - Each omega-regular language can be recognised by a unique minimal layered automaton, admitting a congruence-based description. - This minimal automaton is computable in polynomial time from a given layered automaton. This is a work in progress with Christof Löding and Igor Walukiewicz.

12h00 – 12h25 Gaspard Fougea
Bridging Psychology and Computation: Modular Formalization of Psychological Theories with Automata and Model Checking

Résumé à venir.

12h30 – 12h55 Erwann Loulergue
Passive learning of symbolic automata

Résumé à venir.

Informations pratiques

Les participants recevront des précisions logistiques avant le début des journées.

Les journées auront lieu à l’UPEC à Créteil, Faculté des sciences et technologies-Campus centre. Les 05 et 06 novembre, à l'amphi MSE. Le 07 novembre, (amphi à venir).

Repas : bâtiment (à venir), Faculté des sciences et technologies.

Plan campus central

Accès

Organisation

Dates importantes

Contacts

Groupe de travail GT‑Vérif — https://gt-verif.lis-lab.fr/