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.

PhD Defense: Jawher Jerray

Guaranteed properties of dynamical systems under perturbations
by Jawher Jerray
Friday 10 December 2021 at 11:00
Université Sorbonne Paris Nord, LIPN, Room B107

Jawher Jerray

Abstract: Dynamical systems have a major impact on human development, especially critical systems that can put human lives at risk if something goes wrong. Hence, the need of studying the behavior of these systems to guarantee their correct functioning. Read more...

Matthias Függer et al: new article in JACM

How fast can you converge towards a consensus value?

In their recent work, Matthias Fuegger (LMF), Thomas Nowak (LISN), and Manfred Schwarz (TU Wien) study this question in distributed systems where nodes start from an initial value and seek to converge towards a common consensus value. The paper shows that deceptively simple algorithms are optimal and provides tight lower bounds.

Out now in JACM:

Characterising one-player positionality for infinite duration games on graphs

Speaker: Pierre Ohlmann, IRIF

Tuesday 30 November 2021, 11:00, (Salle 1Z56, bât ENS)

Abstract: I will present a new result, asserting that a winning condition (or, more generally, a valuation) which admits a neutral letter is positional over arbitrary arenas if and only if for all cardinals there exists a universal graph which is monotone and well-founded. Here, "positional" refers only to the protagonist; this concept is sometimes also called "half-positionality".

This is the first known characterization in this setting. I will explain the result, quickly survey existing related work, show how it is proved and try to argue why it is interesting.

Caroline Fontaine Takes the Lead of the CNRS Research Network on Computer Security

Caroline Fontaine at the CNRS-INS2I booth at FIC 2021

Caroline Fontaine has been appointed director of the CNRS Research Network on Computer Security GdR Securité Informatique in Summer 2021. The network federates the French research groups working on cryptography, formal methods for security, privacy, security of hardware, software, data and networks.

The photo shows Caroline at the International Cybersecurity Forum (FIC) on 7 - 9 September in Lille, where she presented the actions of the Network.