News & Events

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.

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.

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

PhD Defense: Yacine El Haddad

Integrating Automated Theorem Provers in Proof Assistants
by Mohamed Yacine El Haddad
Thursday 9 September 2021 at 14h00
online (link to be announced)

Abstract: Lambdapi is a proof assistant that allows users to construct a proof of a given theorem in a universal language based on the lambda-pi-calculus. The goal of this thesis is to add more automation to Lambdapi to save more time and effort for the users.Read more...

PhD defense : Jury Kolčák

Unfoldings and Abstract Interpretation for Parametric Biological Regulatory Networks
by Juraj Kolčák
Tuesday 06 July 2021 at 09h00, online


  • Gilles Bernot (reviewer) – Université Nice Sophia Antipolis, Polytech Nice Sophia
  • Paolo Zuliani (reviewer) – Newcastle University
  • Pascale Le Gall – Centrale Supélec
  • Barbara König – Universität Duisburg-Essen
  • Heike Siebert – Freie Universität Berlin
  • Stefan Haar (PhD Supervisor) – Université Paris-Saclay

Collégiennes et lycéennes à la découverte de l'informatique

L'Université Paris-Saclay organise une école d'été invitant les lycéennes de seconde et collégiennes de 4ème à découvrir les nouvelles sciences.

Le LMF participe à cette initiative avec une présentation des métiers de la recherche et un atelier de robotique avec capteurs. Le but de l'atelier est de concevoir quelques algorithmes distribués simples Read more...

Soutenance de thèse: Gaspard Férey

Gaspard Férey

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

Gaspard Férey

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

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.