News & Events

PhD Defence: Glen Mével

Cosmo: a concurrent separation logic for the weak memory of Multicore OCaml
by Glen Mével
Wednesday 14 December 2022 at 2pm
Inria Paris,. 2 rue Simone Iff, Paris, Salle Lions 1, and online

Abstract: Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code?

To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing non-atomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model.

Read more...

PhD Defence: Amrita Suresh

Formal Verification of Communicating Automata
by Amrita Suresh
Monday 12 December 2022 at 2pm
Room 1Z18, ENS Paris-Saclay and online

Amrita Suresh

Abstract: Distributed systems involve processes that run independently and communicate asynchronously. While they capture a wide range of use cases and are hence, ubiquitous in our world, it is also particularly difficult to ensure their correctness.

In this thesis, we model such systems using mathematical and logical formulation, and try to verify them algorithmically. In particular, we focus on FIFO (First-In First-Out) machines, with one or more finite-state machines communicating via unbounded reliable FIFO buffers. Read more...

PhD Defence: Mathieu Hilaire

Parity games and reachability in infinite-state systems with parameters
by Mathieu Hilaire
Thursday 13 December 2022 at 9am
Room 1Z71, ENS Paris-Saclay and online

Abstract: The most standard model checking approaches are limited to verifying concrete specifications, such as “can we reach a configuration with more than 10 time units elapsing ?”. Nevertheless, for certain computer programs, like embedded systems, the constraints depend on the environment. Thus arises the need for parametric specifications, such as “can we reach a configuration with more than p time units elapsing ?” where p is a parameter which takes values in the non-negative integers.

In this thesis, we study parametric pushdown, counter and timed automata and extensions thereof. In addition to expressing concrete constraints (on the stack, on the counter or on clocks), these can employ parametric constraints. The reachability problem for a parametric automaton asks for the existence of an assignment of the parameters such that there exists an accepting run in the underlying concrete automaton. In addition to the reachability problem, we consider parametric parity games, two player games where players alternate choosing assignments for each parameters, then alternate moving a token along the configurations of the concrete automaton resulting from their choice of parameter assignment. We consider the problem of deciding which player has a winning strategy.

Read more...

Best Process-Mining Dissertation Award for Mathilde Boltenhagen

Mathilde Boltenhagen

Mathilde Boltenhagen received the Best Process Mining PhD Dissertation Award 2022 during the Fourth International Conference on Process Mining (ICPM 2022) for her thesis entitled "Process Instance Clustering based on Conformance Checking Artefacts".

The Best Process Mining PhD Dissertation Award distinguishes theses that contributed to advancing the state of the art in the foundations, engineering, and on-field application of process mining techniques. In this context, the term "process mining" has to be understood in a broad sense: using event data produced during the execution of business, software, or system processes, in order to extract fact-based knowledge and insights on such processes and manage future processes in innovative ways.

Mathilde's thesis contributes to several aspects of conformance checking. It provides a framework and tools to partition log-traces of a process into clusters that use partial-order traces as centroids to take concurrency into account. In her work, Mathilde refined the notion of anti-alignments as a measure for the precision of process model, and she implemented the first efficient approximation of anti-alignments.

Read more...

Portraits de chercheurs : Evelyne Contejean

Evelyne Contejean

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

Portraits de chercheurs : Thomas Nowak

Thomas Nowak

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

Lire l'article

PhD Defence: Gabriel Hondet

Expressing Predicate Subtyping in Computational Logical Frameworks
by Gabriel Hondet
Tuesday 27 September 2022 at 5pm
ENS Paris-Saclay, Room 1Z14

Abstract: Safe programming as well as most proof systems rely on typing. The more a type system is expressive, the more these types can be used to encode invariants which are therefore verified mechanically through type checking procedures. Predicate subtyping extends simple type theory by allowing terms to be defined by predicates. A predicate subtype { x : A | P(x) } is inhabited by terms t of type A for which P(t) holds. This extension provides a rich and intuitive but undecidable type system.

Read more...

Prix Doctorants STIC du plateau de Saclay pour Pierre Vandenhove

Pierre Vandenhove est lauréat d'un accessit au Prix « Doctorants » du plateau de Saclay dans la domaine STIC - Sciences et Technologies de l'Information et la Communication.

Read more...

Nouveau livre : Informatique MPI

Fin août 2022, vient de sortir un nouveau livre par Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyễn, Laurent Sartre.

Il s'intitule "Informatique - MPI2/MPI - CPGE 1re et 2e années: Cours et exercices corrigés" et vise les enseignants d'informatique et les élèves des nouvelles classes préparatoires MP2I et MPI. En voici la table des matières.

En plus de son poids, il faut souligner le site lié qui fournit tous les codes et données du livre.

Philippe Schnoebelen receives LICS 2022 Test-of-Time Award

Philippe Schnoebelen

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.

Lasting impact on the foundations of automatic verification

According to the awarding jury, "This extraordinarily clear and elegant paper provides well-motivated and complete characterizations of succinctness and complexity of linear temporal logic with past operators and with forgettable past. It has contributed to spur a vibrant research program on logics and automata over infinite alphabets, from hardness results to the translations of logical formulas into alternating register automata, along with the attendant powerful algorithmic consequences for model checking. It has also strongly influenced the development of the field of nominal computation, and it is no exaggeration to state that the present paper has tangibly led to a number of invited talks, Dagstuhl-type workshops, research grants, academic positions, and prizes, and continues to have an ongoing and lasting impact in the areas of automata theory and the foundations of automated verification."

The award will be presented at the conference awards session LICS 2022 organized from August 2 to 5 in the framework of FLOC 2022 -- Federated Logic Conference in Haifa, Israel.