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.

The 6th edition of the Workshop on Automata, Concurrency, and Timed Systems will take 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 features a session in honour of Paul Gastin on the occasion of his retirement.

For information on the programme and registration, visit the workshop page.

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

May 23 14:00 ₂₀₂₃

We discuss important characteristics of finite generating sets for F+, the set of all semiflows with non-negative coordinates of a Petri Net. We endeavor to regroup a number of algebraic results dispersed throughout the Petri Nets literature and also to better position the re- sults while considering semirings such as N or Q+ then fields such as Q. As accurately as possible, we provide a range of new algebraic results on minimal semiflows, minimal supports, and finite minimal generating sets for a given family of semiflows. Minimality of semiflows and of sup- port are critical to develop effective analysis of invariants and behavioral properties of Petri Nets. Main results are concisely presented in a table and our contribution is highlighted. We conclude with the analysis of an example drawn from the telecommunication industry underlining the efficiency brought by using minimal semiflows of minimal supports.

Jun 6 14:00 ₂₀₂₃

Robots are expected to play important roles in furthering prosperity, however providing formal guarantees on their (safe) behaviour is not yet fully within grasp given the multifaceted nature of such cyber-physical systems. Simulation, favoured by practitioners, provides an avenue for experimenting with different scenarios before committing to expensive tests and proofs. In this talk, I will discuss how models may be brought together for (co-)verification of system properties, with simulation complementing verification. This will be cast using the model-driven RoboStar framework, that clearly identifies models of the software, hardware, and scenario, and has heterogeneous formal semantics amenable to verification using state-of-the-art model-checkers and theorem provers, such as Isabelle/UTP.

Pedro Ribeiro will be visiting the LMF the entire day - interactions welcome.

Philippe Schnoebelen receives the LICS Test-of-Time Award 2022 for the article Temporal Logic with Forgettable Past co-authored with François Laroussinie (Université Paris-Cité) and Nicolas Markey (IRISA, CNRS). At the time of the writing of the article in 2002, the three authors were members of the same laboratory LSV which integrated the LMF in 2021.

The LICS - Logic in Computer Science conference is the most prestigious annual forum on theoretical and practical topics in computer science related to logic in a broad sense. The LICS Test-of-Time Award award recognizes a small number of papers from the LICS proceedings over the past 20 years (i.e., the paper in question dates from LICS 2002 and was considered this year) that have best stood the "test of time." In selecting these papers, the award committee considers the influence they have had since their publication; due to the fundamental nature of LICS work, the impact is often not felt immediately, hence the 20-year perspective.

Read more...

Jean-​Christophe Filliâtre and Andrei Paskevich have been awarded the prize for the Best Contributed Problem at this year's VerifyThis Competition held as a satelite event of ETAPS 2023.

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.

Gilles Dowek vient d'être nommé au Conseil supérieur des programmes.

Lire l'article

Un article sur Evelyne Contejean vient de paraitre dans la rubrique Portraits de chercheurs des Actualités de l'Université Paris-Saclay.

Lire l'article

Un article sur Thomas Nowak vient de paraitre sur le site de l'ENS Paris-Saclay.

Lire l'article