Launching LMF - the Formal Methods Laboratory

The Laboratoire Méthodes Formelles (LMF) was founded on 1 January 2021 as a joint research centre of University Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, and CentraleSupélec with a main focus on formal methods. The new laboratory combines the expertise of about 100 members from the former Laboratoire Spécification et Vérification (LSV) and the VALS team of Laboratoire de Recherche en Informatique (LRI).

In our mission to enlighten the digital world through Mathematical Logic, we rely on formal methods as a tool to analyse, model, and reason about computing systems, such as computer programs, security protocols, and hardware designs. Our research targets a wide range of computational paradigms, from classical to emerging ones such as biological and quantum computing.

LMF is structured around three hubs: Proofs and Models, which lie at the heart of our historical background, and Interactions, that is aimed at fostering cross-fertilisation between formal methods and other domains in computing science and beyond.

Strategy Complexity of Zero-Sum Games on Graphs

Speaker: Pierre VANDENHOVE

Tuesday, 14 Mars 2023, 14:00, 1Z77

Abstract: In this seminar, I will present the results obtained as part of my PhD thesis cosupervised by Patricia Bouyer at LMF and Mickael Randour at Université de Mons (Belgium). This seminar precedes my thesis defense which will take place in Mons in April. I include here a short abstract; more details are available at my website.

We study zero-sum turn-based games on graphs. Such games can be used to model the interaction between a computer system and its environment, assumed to be antagonistic. The synthesis problem consists in automatically building a controller for the system that guarantees a given objective no matter what happens in the environment, that is, a winning strategy in the derived game.


Philippe Schnoebelen receives LICS 2022 Test-of-Time Award

Philippe Schnoebelen

Philippe Schnoebelen receives the LICS Test-of-Time Award 2022 for the article Temporal Logic with Forgettable Past co-authored with François Laroussinie (Université Paris-Cité) and Nicolas Markey (IRISA, CNRS). At the time of the writing of the article in 2002, the three authors were members of the same laboratory LSV which integrated the LMF in 2021.

The LICS - Logic in Computer Science conference is the most prestigious annual forum on theoretical and practical topics in computer science related to logic in a broad sense. The LICS Test-of-Time Award award recognizes a small number of papers from the LICS proceedings over the past 20 years (i.e., the paper in question dates from LICS 2002 and was considered this year) that have best stood the "test of time." In selecting these papers, the award committee considers the influence they have had since their publication; due to the fundamental nature of LICS work, the impact is often not felt immediately, hence the 20-year perspective.