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.

Two LMF teams winning at VerifyThis Competition

The team of Jean-​Christophe Filliâtre and Andrei Paskevich was recognised Best overall team at this year's VerifyThis Competition. The team of Quentin Garchery and Xavier Denis won the first place for the Best student team award.

VerifyThis is a series of program verification competitions, which takes place annually since 2011. The competition offers a number of challenges presented in natural language and pseudocode. Participants have to formalise the requirements, implement a solution, and formally verify the implementation for adherence to the specification.

Le LMF recherche un·e administrateur·trice systèmes et réseaux

Le laboratoire LMF est en train de constituer l'équipe Systèmes et réseaux qui aura la charge de gérer et de faire évoluer les infrastructures informatiques utilisées quotidiennement pour la recherche, l'enseignement, ainsi que pour les activités de gestion et de communication. L'ingénieur·e d'études recruté·e prendra la direction de cette équipe Systèmes et réseaux.

En savoir plus...

Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic

Speaker: Léon Gondelman, Radbout University, NL

Tuesday 1.6.2021, 11:00, online

Abstract: In this presentation we are going to talk about modular specification and verification of causally-consistent distributed database, a data structure that guarantees causal consistency among replicas of the database.

With causal consistency, different replicas can observe different data on the same key, yet it is guaranteed that all data are observed in a causally related order: if a node N observes an update X originating at node M, then node N must have also observed the effects of any other update Y that took place on node M before X. Causal consistency can, for instance, be used to ensure in a distributed messaging application that a reply to a message is never seen before the message itself.Read more...

EATCS dissertation Award for Marie Fortin

Marie Fortin

Marie Fortin received the EATCS Distinguished Dissertation Award for 2020. The award established by the European Association of Theoretical Computer Science recognises outstanding dissertations in the field of Theoretical Computer Science.

Marie prepared her thesis Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata at LSV under the supervision of Benedikt Bollig and Paul Gastin.

Serge Haddad co-chairing CONCUR

Serge Haddad is co-chairing CONCUR 2021 organised as part of the QONFEST 2021 conference which federates four main venues in the area of formal methods:

  • CONCUR 2021, the 32st International Conference on Concurrency Theory
  • FMICS 2021, the 26th International Conference on Formal Methods for Industrial Critical Systems
  • FORMATS 2021, the 19th International Conference on Formal Modeling and Analysis of Timed Systems
  • QEST 2021, the 18th International Conference on Quantitative Evaluation of SysTems