Editorial

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.

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

Events

Journée Méthodes de Test pour la Vérification et la Validation

Jeudi, 16 Mars 2023
Accueil : espace SIMONON, Salle 1E19, bâtiment Sud-Ouest ENS Paris-Saclay
Exposés : Salle 1Z28, bâtiment Nord ENS Paris-Saclay (éventuellement 1B18)
Lien visio : Zoom (Meeting ID: 994 7419 3300, Passcode: 89821603)

MTV2

Larencontre annuelle du groupe de travail MTV2 Méthodes de Test pour la Vérification et la Validation sera organisée au LMF par Burkhart Wolff, Frédéric Voisin et Fatiha Zaidi le 16 mars 2023,

Read more...

By patricia, on March 03, 2023, at 04:54 PM

Seminar

A Gentle Introduction to Matching Logic and its Applications

Speaker: Dorel Lucanu

Tuesday, 28 March 2023, 14:00, 1Z56 New date: Wednesday, 29 March 2023, 14:00, hybrid

Abstract: Matching Logic (ML) allows to uniformly specify and reason about programming languages and properties of their programs. It was developed as a logical foundation of the K framework.

ML is expressive enough to specify all properties within various logical systems such as FOL, separation logic,  lambda-calculus, (dependent) type systems, and modal  mu-calculus. In particular, it supports operational semantics (term rewriting) and axiomatic semantics (Hoare triples). ML has a sound  fixed Hilbert-style proof system that supports formal reasoning for all specifications. In this talk we give a gentle introduction to (Applicative) Matching Logic [3], we show how the initial algebraic semantics can be encoded as ML theories [4], and how ML is used to formaly define programming languages semantics and program properties.

Read more...

By BurkhartWolff, on February 01, 2023, at 05:54 PM

Awards

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.

Read more...

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