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.

Xavier Denis, ancien doctorant du LMF, encadré par Jacques-Henri Jourdan et Claude Marché, a reçu le prix de thèse du GdR Génie de la Programmation et Logiciel, décerné mardi 5 juin lors des journées nationales du GdR.

Sa thèse est intitulée Deductive Verification for Rust Programs. Félicitations à Xavier pour son excellent travail !

Plus d'informations sur le site du GdR.

Jun 19 14:00 ₂₀₂₄

The Semantics of Effects: Centrality, Quantum Control, and Reversible Recursion

Mercredi 19 juin 2024 à 14h

ENS Paris-Saclay, Amphithéâtre Lagrange, salle 1Z14 and online.

My manuscript is available here.

Résumé. Le sujet de cette thèse est axé sur la théorie des langages de programmation. Dans un langage de programmation suffisamment bien défini, le comportement des programmes peut être étudié à l'aide d'outils empruntés à la logique et aux mathématiques, énonçant des résultats sans exécuter le code.

Ce domaine de l'informatique est appelé "sémantique". La sémantique d'un langage peut se présenter sous plusieurs formes : dans notre cas, des sémantiques opérationnelles, des théories équationnelles et des sémantiques dénotationnelles. Read more...

Jun 21 9:30 ₂₀₂₄

Title: Polymorphic type inference for dynamic languages: reconstructing types for systems combining parametric, ad-hoc, and subtyping polymorphism

Friday, June 21th at 09:30 (Paris time, UTC+2)
Batiment Sophie Germain, 3rd floor, Room 3052 8 Pl. Aurélie Nemours, 75013 Paris

Zoom link: https://u-paris.zoom.us/j/83379216296?pwd=ZxYiEqpCprbs9leonLXgEbniPVmwXs.1 Meeting ID: 833 7921 6296 Passcode: 341938

Abstract. Programming languages can be broadly categorized into two groups: static languages, such as C, Rust, and OCaml, and dynamic languages, such as Python, JavaScript, and Elixir. While static languages generally offer better performance and more security thanks to a phase of static typing that precedes compilation ("well-typed programs cannot go wrong"), this often comes at the expense of flexibility, making programs safer but prototyping more tedious. In this defence, I present a formal system for statically typing dynamic languages, offering a compromise between safety and flexibility.

Read more...

Measuring Well Quasi-Orders and Complexity of Verification

Jul 3 14:00 ₂₀₂₄

Mercredi 3 juillet 2024 à 14h

ENS Paris-Saclay, salle 1Z18, Lien Zoom.

Abstract. We investigate three ordinal measures of a well quasi-order, also called ordinal invariants: maximal order type, width, and height. One main challenge is to compute the ordinal invariants of complex well quasi-orders built from simpler well quasi-orders through classical operation, such as the Cartesian product, and high-order constructions, like the finite words embedding.

In this thesis, we compute compositionally the maximal order type of the direct product, the width of the multiset embedding, and the height and width of the multiset ordering. Furthermore, we compute the width of the Cartesian product in restricted cases and prove tight bounds on the ordinal measures of the finite powerset. Read more...

Prétraitement compositionnel en Coq

Jul 10 14:00 ₂₀₂₄

Mercredi 10 juillet 2024 à 14h

ÉNS Paris-Saclay, salle 1Z31, Lien Zoom.

Abstract. This thesis presents a new methodology for preprocessing goals in the Coq proof assistant in order to send them to an automatic solver. This methodology consists of composing atomic and certifying transformations based on the goal to be proven. We will first present the library of transformations that we have written, then we will present an orchestrating tool for these transformations, which aims to be generic. This has led to the implementation of a new 'push-button' tactic called 'snipe' for Coq.

Read more...

An Ontology Framework for Formal Libraries

Jul 12 13:30 ₂₀₂₄

Vendredi 12 juillet 2024 à 13:30h, Batiment 650, 435 (Salle des Theses).

Abstract.

Document ontologies, i. e., a machine-readable form of the structure of documents as well as the document discourse, play a key role in structuring the link between semantic notions and documents containing infor- mal text. In many scientific disciplines such as medicine or biology, ontologies allows the organization of research papers and their automated access. There are particular challenges in the field mathematics and engineering where documents contain both formal and informal text- elements with a complex structure of mutual links and dependencies of various types. Texts may contain formulas (which should be at least type-correct and if possible semantically consistent with the formal definitions) and formal definitions based on naming conventions that should reflect informal explanations. A deeper access into the formal parts of this type of documents involves a framework that can cope with typed, logical languages, which requires going substantially further than existing ontological languages like, for example, OWL.

Read more...

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

May 23 14:00 ₂₀₂₄

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.

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

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