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.

The 6th edition of the Workshop on Automata, Concurrency, and Timed Systems will take place from 30 May to 2 June 2023 at ENS Paris-Saclay.

The workshop series emerged from a long-standing Indo-French cooperation in the areas of ACTS: Automata and Logic, Concurrency Theory, and Timed Systems.

As a special event, this year's programme features a session in honour of Paul Gastin on the occasion of his retirement.

For information on the programme and registration, visit the workshop page.

Oct 12 14:00 ₂₀₂₃

Read more...

Sep 12 14:00 ₂₀₂₃

Quantum computing aims at addressing computations that are currently intractable by conventional supercomputers but it is also a promising technology for speeding up some existing simulations. However it is commonly accepted that quantum algorithms will be essentially ``hybrid'' with some tasks being executed on the quantum processor while others will remain treated on classical processors (CPU, GPU,...). Among the crucial tasks achieved on classical computers, several require efficient linear algebra algorithms.

Read more...

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.

Read more...

Congratulations to Jacques-Henri Jourdan and his co-authors who will receive the 2023 Alonzo Church Award for their outstanding contributions to Logic and computation with the design and implementation of Iris, a higher-order concurrent separation logic framework. The Award will be presented at the 50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023, in July.

Iris has been widely used in academia, and also in industry, e.g., by engineers at Meta to verify the core components of an interprocess communication system for a new operating system.

Read more...

Gilles Dowek vient d'être nommé au Conseil supérieur des programmes.

Lire l'article

Un article sur Evelyne Contejean vient de paraitre dans la rubrique Portraits de chercheurs des Actualités de l'Université Paris-Saclay.

Lire l'article

Un article sur Thomas Nowak vient de paraitre sur le site de l'ENS Paris-Saclay.

Lire l'article