# News & Events

## Journée *Méthodes de Test pour la Vérification et la Validation*

Jeudi, 16 Mars 2023**Accueil :** espace SIMONON, Salle 1E19, bâtiment Sud-Ouest ENS Paris-Saclay **Exposés : Salle 1Z28**, bâtiment Nord ENS Paris-Saclay (éventuellement 1B18) **Lien visio : ** Zoom
(Meeting ID: 994 7419 3300, Passcode: 89821603)

Larencontre annuelle du groupe de travail MTV2 Méthodes de Test pour la Vérification et la Validation sera organisée au LMF par Burkhart Wolff, Frédéric Voisin et Fatiha Zaidi le 16 mars 2023,

## PhD Defence: Agustín Borgna

Towards a formal compilation stack-frame in quantum computing

by Agustín Borgna

Friday 13 January 2023 at 3pm

Loria, Nancy and online

**Abstract:**
The advent of quantum computers capable of solving problems that are intractable on classical computers has motivated the development of new programming languages and tools for quantum computing. However, the current state of the art in quantum programming is still in its infancy.

In this thesis, we present a series of novel approaches to different aspects of the quantum compilation process based on the ZX calculus. Read more...

## PhD Defence: Kostia Chardonnet

Towards a Curry-Howard Correspondence for Quantum Computation

by Kostia Chardonnet

Monday 9 January 2023 at 2pm

Salle des thèses, PCRI and online

**Abstract:**
In this thesis, we are interested in the development of a Curry-Howard
correspondence for quantum computing, allowing to represent quantum types and
quantum control-flow. In the standard model of Quantum Computation, a classical
computer is linked to a quantum coprocessor. The classical computer can then
send instructions to allocate, update, or read quantum registers. The programs
executed by the coprocessor are represented by a quantum circuit: a sequence of
instructions that applies unitary operations to the input quantum bits. Read more...

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

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

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

## Best Process-Mining Dissertation Award for 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".

## Portraits de chercheurs : Evelyne Contejean

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