Création du Laboratoire Méthodes Formelles

Le Laboratoire Méthodes Formelles (LMF) est né le 1er janvier 2021 de la volonté politique de ses tutelles - Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria et CentraleSupélec - de créer un pôle ciblé sur les méthodes formelles. Le LMF est formé du Laboratoire Spécification et Vérification (LSV, ENS Paris-Saclay, CNRS, Inria) et de l’équipe Vals du Laboratoire de Recherche en Informatique (LRI, Université Paris-Saclay, CNRS, Inria, CentraleSupélec) soit une centaine de personnes.

Son ambition est d’éclairer le « monde numérique » grâce à la logique mathématique en utilisant les méthodes formelles comme outil d’analyse, de modélisation et de raisonnement pour les programmes informatiques, les protocoles de sécurité, etc. Il s'appuie sur des paradigmes de calcul des plus classiques aux plus novateurs comme l’informatique quantique.

Le LMF est structuré en pôles : son cœur de métier en comporte deux, « Preuves » et « Modèles » ; le troisième, « Interactions », est une ouverture à d’autres domaines tels que l’IA et la biologie.

PhD Defense: Anirban Majumdar

Verification and Synthesis of Parameterized Concurrent Systems
by Anirban Majumdar
Thursday 30 September 2021 at 14h00
room 1Z68 ENS Paris-Saclay as well as online (link to be posted)

Anirban Majumdar

Abstract: This thesis is at the crossroad of verification and synthesis of parameterized concurrent systems. The parameterized model checking problem asks whether a system satisfies a given specification independently of the number of its components, whereas synthesis requires an algorithmic design of protocols for its components so that the specification is satisfied.Read more...

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.

Best-Paper Award at FMICS 2021

Cláudio Belo Lourenço and Claude Marché from the Toccata team at LMF with co-authors from Mitsubishi Electric received the Best-Paper Award at FMICS 2021, the 26th International Conference on Formal Methods for Industrial Critical Systems.

Their contribution Automated Verification of Temporal Properties of Ladder Programs was valued by the jury as a "good example for how formal methods can be used in industrial applications" with "industrial interest for both legacy Ladder programs and programs to be developed".

FMICS 2021 was held as part of the QONFEST event that federated four main venues in the area of formal methods.

Towards Security-Oriented Program analysis

Speaker: Sébatien Bardin, CEA, Paris-Saclay

Tuesday 7 September 2021, 11:00, (amphi 1Z53, ENS Paris-Saclay)

Abstract: While digital security concerns increase, we face both a urging demand for more and more code-level security analysis and a shortage of security experts. Hence the need for techniques and tools able to automate part of these code-level security analyses. As source-level program analysis and formal methods for safety-critical applications have made tremendous progress in the past decades, it is extremely tempting to adapt them from safety to security. Yet, security is not safety and, while still useful, a direct adaptation of safety-oriented program analysis to security scenarios remains limited in its scope. In this talk, we will argue for the need of security-oriented program analysis. We will first present some of the new challenges faced by formal methods and program analysis in the context of code-level security scenarios. For example, security-oriented code analysis is better performed at the binary level, the attacker must be taken into account and practical security properties deviate from standard reachability / invariance properties. Second, we will discuss some early results and achievements carried out within the BINSEC group at CEA LIST. Especially, we will show how techniques such as symbolic execution and SMT constraint solving can be tailored to a number of practical code-level security scenarios.

Best-Paper Award at ICTAC 2021

Diaz, Dowek - ICTAC 2021 Best Paper Award

Gilles Dowek and Alejandro Díaz-Caro (Universidad de Buenos Aires and Universidad Nacional de Quilmes, Argentina) received the Best-Paper Award at ICTAC 2021, the 18th International Colloquium on Theoretical Aspects of Computing for their paper A New Connective in Natural Deduction, and Its Application to Quantum Computing.

EATCS dissertation Award for Marie Fortin

Marie Fortin

Marie Fortin received the EATCS Distinguished Dissertation Award for 2020. The award established by the European Association of Theoretical Computer Science recognises outstanding dissertations in the field of Theoretical Computer Science.

Marie prepared her thesis Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata at LSV under the supervision of Benedikt Bollig and Paul Gastin.