News & Events
Soutenance de thèse: Gaspard Férey
Higher-Order Confluence and Universe Embedding in the Logical Framework
par Gaspard Férey
mercredi, 30 juin 2021 à 10h00
Résumé : La multiplicité des systèmes formels a mis en évidence la nécessité d'un socle logique commun dans lequel les formalismes logiques pourraient être exprimés. L'enjeu principal de ce manuscrit est la définition de techniques d'encodages reposant sur la réécriture de termes et capables de représenter les fonctionnalités avancées des systèmes de types modernes. Read more...
PhD Defense: Gaspard Férey
Higher-Order Confluence and Universe Embedding in the Logical Framework by: Gaspard Férey Wednesday 30 June 2021, 10:00 remote
Summary: In the context of the multiplicity of formal systems, it has become a growing need to express formal proofs into a common logical framework. This thesis focuses on the use of higher-order term rewriting to embed complex formal systems in the simple and well-studied lambda-Pi calculus modulo. Read more...
EATCS dissertation Award for 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.
Portraits de chercheurs : Patricia Bouyer
Un article sur Patricia Bouyer vient de paraitre dans la rubrique Portraits de chercheurs des Actualités de l'Université Paris-Saclay.
Actualité INS2I-CNRS sur Why3, le programme qui vérifie les programmes
La plateforme Why3 développé au LMF est au sujet d'un article apparu dans les Actualités de l'INS2I-CNRS à la suite d'un entretien avec Jean-Christophe Filliâtre.
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.
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.
Renaud Vilmart - Il était une fois… ma thèse
Renaud Vilmart illustre sa thèse dans l'article Ordinateur quantique : quand un petit dessin vaut mieux qu’un long code apparu sous la rubrique Il était une fois… ma thèse du Blog BINAIRE.
Renaud est lauréat d’un accessit au prix de thèse décerné par la SiF et patronné par l’Académie des Sciences pour sa thèse ZX-Calculs pour l’Informatique Quantique et leur Complétude.
Two LMF teams winning at VerifyThis Competition
The team of Jean-Christophe Filliâtre and Andrei Paskevich was recognised Best overall team at this year's VerifyThis Competition. The team of Quentin Garchery and Xavier Denis won the first place for the Best student team award.
VerifyThis is a series of program verification competitions, which takes place annually since 2011. The competition offers a number of challenges presented in natural language and pseudocode. Participants have to formalise the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
Serge Haddad co-chairing CONCUR
Serge Haddad is co-chairing CONCUR 2021 organised as part of the QONFEST 2021 conference which federates four main venues in the area of formal methods:
- CONCUR 2021, the 32st International Conference on Concurrency Theory
- FMICS 2021, the 26th International Conference on Formal Methods for Industrial Critical Systems
- FORMATS 2021, the 19th International Conference on Formal Modeling and Analysis of Timed Systems
- QEST 2021, the 18th International Conference on Quantitative Evaluation of SysTems