Agenda

Département
Langue
Date
Thématique
2025

novembre

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

décembre