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.

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

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

MT180s : Gaspard Fougea reçoit le prix du jury à la finale Université Paris-Saclay

Toutes nos félicitations à Gaspard Fougea pour le prix du jury reçu à la finale Université Paris-Saclay du concours Ma thèse en 180 secondes.

Gaspard prépare sa thèse « Modèles formels pour la conscience : de l’expérience subjective aux algorithmes cognitifs » au LMF sous la direction d'Alain Finkel et Stéphane le Roux.

https://www.youtube.com/watch?v=SYZ5LvZieOA

Keynote: Challenges and triumphs of verification in the CSP style

Speaker: Bill Roscoe Emeritus professor, University of Oxford, GB

Thursday (!) May 23 2024, 14:00, Room 1Z56

Abstract: I have been doing practical verification in CSP, its tools and models for 40 years. The main challenge has been packaging this for the industrial engineer. I will discuss how this has been solved in the Coco System www.cocotec.io, which is used for object based development of massive systems in industry. Separately I will show how I have used it to underpin a highly innovative blockchain consensus protocol by using it to model decentralised, partly malevolent systems.

Static analysis and model reduction for a site-graph rewriting language

Speaker: Jérôme Feret ENS Ulm, jerome.feret@ens.psl.eu

Tuesday Mar 26 2024, 14:00, Room 1Z56

Abstract: Software sciences have a role to play in the description, the organization, the execution, and the analysis of the molecular interaction systems such as biological signaling pathways. These systems involve a huge diversity of bio-molecular entities whereas their dynamics may be driven by races for shared resources, interactions at different time- and concentration-scales, and non-linear feedback loops. Understanding how the behavior of the populations of proteins orchestrates itself from their individual interactions, which is the holy grail on systems biology, requires dedicated languages offering adapted levels of abstraction and efficient analysis tools.

In this talk we describe the design of formal tools for Kappa, a site-graph rewriting language inspired by bio-chemistry. In particular, we introduce a static analysis to compute some properties on the biological entities that may arise in models, so as to increase our confidence in them. We also present a model reduction approach based on a study of the flow of information between the different regions of the biological entities and the potential symmetries. This approach is applied both in the differential and in the stochastic semantics.

Gilles Dowek lauréat du Grand prix Inria - Académie des sciences 2023

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

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.

Read more...

Hubert Comon-Lundh receives LICS 2023 Test-of-Time Award

Hubert Comon-Lundh

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