Création du Laboratoire Méthodes Formelles

Le Laboratoire Méthodes Formelles (LMF) est né le 1er janvier 2021 de la volonté politique de ses tutelles - Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria et CentraleSupélec - de créer un pôle ciblé sur les méthodes formelles. Le LMF est formé du Laboratoire Spécification et Vérification (LSV, ENS Paris-Saclay, CNRS, Inria) et de l’équipe Vals du Laboratoire de Recherche en Informatique (LRI, Université Paris-Saclay, CNRS, Inria, CentraleSupélec) soit une centaine de personnes.

Son ambition est d’éclairer le « monde numérique » grâce à la logique mathématique en utilisant les méthodes formelles comme outil d’analyse, de modélisation et de raisonnement pour les programmes informatiques, les protocoles de sécurité, etc. Il s'appuie sur des paradigmes de calcul des plus classiques aux plus novateurs comme l’informatique quantique.

Le LMF est structuré en pôles : son cœur de métier en comporte deux, « Preuves » et « Modèles » ; le troisième, « Interactions », est une ouverture à d’autres domaines tels que l’IA et la biologie.

The Skolem Landscape

Speaker: Joël Ouaknine, Max Planck Institute for Software Systems, Saarbrücken, Germany

Tuesday Dec 13 2022, 14:00, Room 1Z56

Abstract: The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science. Unfortunately, the decidability of the Skolem Problem has been open for nearly a century! In this talk, I will present a survey of what is known on this problem and related questions, including recent and ongoing developments.

Best Process-Mining Dissertation Award for Mathilde Boltenhagen

Mathilde Boltenhagen

Mathilde Boltenhagen received the Best Process Mining PhD Dissertation Award 2022 during the Fourth International Conference on Process Mining (ICPM 2022) for her thesis entitled "Process Instance Clustering based on Conformance Checking Artefacts".

The Best Process Mining PhD Dissertation Award distinguishes theses that contributed to advancing the state of the art in the foundations, engineering, and on-field application of process mining techniques. In this context, the term "process mining" has to be understood in a broad sense: using event data produced during the execution of business, software, or system processes, in order to extract fact-based knowledge and insights on such processes and manage future processes in innovative ways.

Mathilde's thesis contributes to several aspects of conformance checking. It provides a framework and tools to partition log-traces of a process into clusters that use partial-order traces as centroids to take concurrency into account. In her work, Mathilde refined the notion of anti-alignments as a measure for the precision of process model, and she implemented the first efficient approximation of anti-alignments.

Read more...

PhD Defence: Amrita Suresh

Formal Verification of Communicating Automata
by Amrita Suresh
Monday 12 December 2022 at 2pm
Room 1Z18, ENS Paris-Saclay and online

Amrita Suresh

Abstract: Distributed systems involve processes that run independently and communicate asynchronously. While they capture a wide range of use cases and are hence, ubiquitous in our world, it is also particularly difficult to ensure their correctness.

In this thesis, we model such systems using mathematical and logical formulation, and try to verify them algorithmically. In particular, we focus on FIFO (First-In First-Out) machines, with one or more finite-state machines communicating via unbounded reliable FIFO buffers. Read more...

PhD Defence: Mathieu Hilaire

Parity games and reachability in infinite-state systems with parameters
by Mathieu Hilaire
Thursday 13 December 2022 at 9am
Room 1Z71, ENS Paris-Saclay and online

Abstract: The most standard model checking approaches are limited to verifying concrete specifications, such as “can we reach a configuration with more than 10 time units elapsing ?”. Nevertheless, for certain computer programs, like embedded systems, the constraints depend on the environment. Thus arises the need for parametric specifications, such as “can we reach a configuration with more than p time units elapsing ?” where p is a parameter which takes values in the non-negative integers.

In this thesis, we study parametric pushdown, counter and timed automata and extensions thereof. In addition to expressing concrete constraints (on the stack, on the counter or on clocks), these can employ parametric constraints. The reachability problem for a parametric automaton asks for the existence of an assignment of the parameters such that there exists an accepting run in the underlying concrete automaton. In addition to the reachability problem, we consider parametric parity games, two player games where players alternate choosing assignments for each parameters, then alternate moving a token along the configurations of the concrete automaton resulting from their choice of parameter assignment. We consider the problem of deciding which player has a winning strategy.

Read more...

PhD Defence: Glen Mével

Cosmo: a concurrent separation logic for the weak memory of Multicore OCaml
by Glen Mével
Wednesday 14 December 2022 at 2pm
Inria Paris,. 2 rue Simone Iff, Paris, Salle Lions 1, and online

Abstract: Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code?

To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing non-atomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model.

Read more...

LICS Test-of-Time Award pour Philippe Schnoebelen

Philippe Schnoebelen

Philippe Schnoebelen reçoit le LICS Test-of-Time Award 2022 pour l'article Temporal Logic with Forgettable Past cosigné avec François Laroussinie (Université Paris-Cité) et Nicolas Markey (IRISA, CNRS). Au moment de la rédaction de l'article en 2002, les trois auteurs étaient membres du même laboratoire LSV qui a intégré le LMF en 2021.

La conférence LICS — Logic in Computer Science est le plus prestigieux forum annuel sur des sujets théoriques et pratiques en informatique liés à la logique au sens large. Le prix LICS Test-of-Time Award récompense un petit nombre d'articles tirés des actes du LICS des 20 dernières années (c'est-à-dire que l'article en question date du LICS 2002 et a été pris en considération cette année) qui ont le mieux résisté à "l'épreuve du temps”. En sélectionnant ces articles, le comité d'attribution tient compte de l'influence qu'ils ont eue depuis leur publication ; en raison de la nature fondamentale des travaux de la LICS, l'impact n'est souvent pas ressenti immédiatement, d'où la perspective de 20 ans.

Read more...