Agenda

Département
Langue
Date
Thématique
2025

novembre

  • 14:00
    15: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çais
    LaBRI, salle 178
  • 10:45
    11: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

    https://combalgo.labri.fr/pmwiki.php/Groupe/Info-Quantique

    Français
    Room 178
  • 12:45
    13: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:00
    14: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çais
    LaBRI, salle 178
  • 16:00
    18: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.

    English
    Amphi LaBRI
  • 09:30
    10: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