Agenda
novembre
-
14:0015:00
I am interested in verification of distributed systems with an unbounded number of agents running the same finite-state program. These include systems like conservative Petri nets, population protocols, reconfigurable broadcast networks and more. Properties of interest for these systems are "parameterized": for example, is there a number of agents N such that my system instantiated with N agents reaches a bad configuration? I will present a recent result on HyperLTL for population protocols, where we will see that the verification problem can be cast as a parameterized reachability property. I will then present some open questions for parameterized verification of such systems. If I have time, I will present my newest research direction which concerns runtime verification of distributed systems, and the hypotheses that can be made on the setting.
FrançaisLaBRI, salle 178 -
10:4511:45
The edge list model is arguably the simplest input model for graphs, where the graph is specified by an unordered list of its edges. In this model, we study the quantum query complexity of k-cycle finding, and its connections with k-distinctness. Specifically, given any graph with low maximum degree, such as a typical random sparse graph, we prove that the quantum query complexity of finding a length-k cycle in its length-m edge list is m^{3/4-1/(2^{k+2}-4) ± o(1)}, which matches the best-known upper bound for the quantum query complexity of k-distinctness on length-m inputs up to an m^{o(1)} factor. We prove the lower bound by developing new techniques within Zhandry's recording query framework (cryptology eprint: 2018/276) as generalized by Hamoudi and Magniez (arxiv: 2002.08944). These techniques extend the framework to treat any non-product distribution that results from conditioning a product distribution on the absence of rare events. We prove the upper bound by adapting Belovs's learning graph algorithm for k-distinctness (arxiv: 1205.1534). Finally, assuming a plausible conjecture concerning only cycle finding, we show that the lower bound can be lifted to an essentially tight lower bound on the quantum query complexity of k-distinctness, which is a long-standing open question.
Based on arxiv: 2412.17786
FrançaisRoom 178 -
12:4513:45
Michel Le Van Kiem (Grand Port Maritime de Bordeaux) donnera un séminaire, le 20 novembre 2025 de 12h45 à 13h45, amphi du LaBRI.
L’intitulé du séminaire : « Les communs numériques : une réponse aux enjeux sociétaux actuels ? ».
Amphi LaBRI -
13:0014:00
The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs has remained stubbornly open for a decade. We recently shown its undecidability. However, the Value problem is decidable for a subclass of two-clock weighted timed games.
FrançaisLaBRI, salle 178 -
16:0018:00
Avec l'arrivée de l'exascale, les modèles de programmation parallèle tendent à masquer les détails de la machine en exposant le matériel au niveau logiciel avec le modèle PGAS (Partitioned Global Address Space). La norme MPI (Message Passing Interface) propose un modèle de communication similaire, via les communications unilatérales MPI. Ces opérations permettent un meilleur recouvrement des communications par les calculs par rapport aux communications bilatérales classiques. Cependant, les programmeurs doivent gérer la cohérence et la synchronisation des données pour éviter les conflits d'accès aux données, ce qui peut s'avérer difficile. Notre étude propose deux solutions pour faciliter l'utilisation des communications unilatérales dans les programmes MPI. La première consiste à améliorer un outil vérifiant la cohérence mémoire pour une meilleure mise à l'échelle. La seconde est un outil transformant automatiquement les communications bilatérales en communications unilatérales.
EnglishAmphi LaBRI -
09:3010:30
Les bibliothèques de code vérifié par machine sont aujourd'hui organisées autour de hiérarchies de structures algébriques. Malheureusement, le langage de la théorie des types et les fonctionnalités fournies par le système Coq rendent la construction d'une hiérarchie difficile, même pour les utilisateurs experts. La difficulté commence par les choix non orthogonaux, entre le stockage des informations sous forme de champs d'enregistrement ou de paramètres, et entre l'utilisation de classes de types et de structures canoniques pour l'inférence. A cela s'ajoutent les préoccupations relatives aux performances et à la facilité d'utilisation, par un non-expert, de la hiérarchie finale.
HB fournit au concepteur de bibliothèques un langage permettant de décrire les éléments constitutifs des structures algébriques et de les assembler en une hiérarchie. De même, il fournit à l'utilisateur final des constructions linguistiques pour créer des instances (exemples) de structures et pour enseigner à l'élaborateur de Coq comment tirer parti de ces connaissances lors de l'inférence de types. Enfin, HB permet au concepteur de la bibliothèque d'améliorer la facilité d'utilisation de sa bibliothèque en fournissant des interfaces alternatives aux interfaces primitives, une fonctionnalité qui peut également être utilisée pour s'adapter aux changements apportés à la hiérarchie sans perturber le code utilisateur.
Il s'agit d'un travail conjoint avec Kazuhiko Sakaguchi, Pierre Roux et Enrico Tassi.
Salle 76
décembre
-
11:0012:00
Mouna Safir (ENS Lyon)
Title: Fault tolerance in distributed systems
Abstract:
One of the key principles of distributed computing is to replicate data and distribute tasks to improve the availability and fault-tolerance. But this distribution poses new challenges, in particular the coordination of processes. To ensure the consistency and proper functioning of the system, distributed entities must exchange information and reach joint decisions, even in the case of breakdowns or unpredictable behaviour. In this context, fault-tolerance becomes a central issue. Distributed systems must continue to operate despite partial failures or abnormal behaviours of certain components.
In my research, I explored two ways to strengthen the resilience of distributed systems:
- The k-agreement, which makes it possible to ensure coordination despite the faults.
- Self-stabilization, which aims to automatically restore the system after temporary disturbances.In the course of my presentation, I will present the main results achieved in these two lines of research.
FrançaisLaBRI 178 -
14:0015:00
to be announced
FrançaisLaBRI, salle 178 -
12:4513:45
Mohamed Mosbah (Bx INP, LaBRI) donnera un séminaire, le 04 Mos
Amphi LaBRI -
15:3018:30
Clément Gaspard soutiendra sa thèse, le 08 décembre 2025 à 15h30, dans l’amphi 2 du Bât 2A de l’IUT de Bordeaux (Gradignan).
L’intitulé de sa thèse est : « Locomotion, planification de pas et résistance aux chutes des robots humanoïdes via des politiques d’apprentissage par renforcement ».
Amphi 2 Bât 2A (IUT de Bx, Gradignan)