LMF Main/Accueil

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.

By dwb, on January 01, 2021, at 05:41 PM

Événements

ACTS 2023 - Workshop on Automata, Concurrency, and Timed Systems

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.

By dwb, on April 26, 2023, at 02:32 PM

Événements

Soutenance de thèse : Aliaume Lopez

Oct 12 14:00 ₂₀₂₃

First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions
par Aliaume Lopez
Mardi 12 septembre 2023 à 14h
Université Paris-Cité, Bâtiment Olympe de Gouges, salle 127

By aliaume, on September 08, 2023, at 09:28 AM

Séminaire

Some challenges in quantum computing for linear algebra algorithms and data structures

Sep 12 14:00 ₂₀₂₃

Speaker: Marc Baboulin, Université Paris-Saclay

Tuesday, 12 September 2023, 14:00, Room 1Z34

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.

By Patricia, on August 30, 2023, at 10:45 PM

Distinctions

LICS Test-of-Time Award pour 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.

By dwb, on July 30, 2022, at 08:00 AM

Distinctions

Alonzo Church Award 2023 for Jacques-Henri Jourdan

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.