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 took 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 featured a session in honour of Paul Gastin on the occasion of his retirement.

Read more...

Stéphane Demri (LMF, CNRS) and Karin Quaas (Leipzig University) received the Best-Paper Award at JELIA 2023, the 18th Edition of the European Conference on Logics in Artificial Intelligence, which is a major forum for logic-based approaches to AI. Read more...

Dec 12 14:00 ₂₀₂₃

Abstract: In recent years a wealth of logic-based languages have been introduced to reason about the strategic abilities of autonomous agents in multi-agent systems. This talk presents some of these important logical formalisms, namely, the Alternating-time Temporal Logic and Strategy Logic. We discuss recent extensions of those formalisms to capture different degrees of satisfaction, as well as to handle uncertainty caused by the partial observability of agents and the intrinsic randomness of MAS. Finally, we describe the recent application of those formalisms for Mechanism Design and explain how they can be used either to automatically check that a given mechanism satisfies some desirable property, or to produce a mechanism that does it.

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...

Le Grand prix 2023 Inria-Académie des sciences a été décerné à Gilles Dowek.

Parallèlement à ses travaux scientifiques et techniques, Gilles Dowek a contribué à la construction d'une philosophie naissante de l'informatique, qui se construit dans un dialogue entre philosophes et scientifiques. Il s'est, en particulier, intéressé à la place du calcul en mathématiques, à la différence entre les langues et les langages et aux rapports entre la thèse de Church-Turing et celle de Galilée.

— Citation du prix

Le Prix Inria – Académie des sciences récompense depuis 2013 une ou un scientifique ayant contribué de manière exceptionnelle au champ des sciences informatiques et mathématiques.

Read more...

Hubert Comon-Lundh received the LICS Test-of-Time Award 2023 for the article Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive Or (ArXiv preprint) co-authored with Vitaly Shmatikov (SRI International). The award was shared with the related paper An NP Decision Procedure for Protocol Insecurity with XOR by Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, and Mathieu Turuani.

Cryptographic protocols rely on cryptographic primitives to achieve goals such as data privacy and data authenticity in the presence of an attacker. Their use in important applications such as communications over the Internet or credit card payments calls for the automated verification of their security. These two papers made important progress on algorithmic aspects of protocol verification with additional operators, including XOR which is widely used in real-life applications.

Specifically, these papers establish the decidability of insecurity of cryptographic protocols with XOR and other equational theories. Chevalier et al. prove membership in NP when restricted to XOR, while Comon and Shmatikov prove decidability in a broader setting. In addition to definitively settling the complexity question for these cases, the lasting value of this line of work is demonstrated by mature verification tools such as ProVerif, Tamarin, Maude-NPA, and CPSA.— Jury Laudation

Read more...

Gilles Dowek a été nommé membre, en tant que personnalité qualifiée, au Conseil supérieur des programmes.

Le Conseil supérieur des programmes est une instance indépendante placée auprès du ministre de l’Éducation nationale et la Jeunesse. Il doit offrir les garanties scientifiques nécessaires pour émettre des avis et formuler des propositions dans ses champs de compétences.

Read more...