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

  • 11:00
    12: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.

    https://algodist.labri.fr/index.php/Main/GT

    Français
    LaBRI 178
  • 14:00
    15:00

    to be announced

    Français
    LaBRI, salle 178
  • 12:45
    13:45

    Mohamed Mosbah (Bx INP, LaBRI) donnera un séminaire, le 04 Mos
     

    Amphi LaBRI
  • 14:00
    17:00

    L’adoption du dossier patient informatisé a considérablement amélioré l’accès à de vastes volumes de données cliniques. Si cet accès constitue une ressource précieuse pour les soins comme pour la recherche, il soulève néanmoins de nouveaux défis liés à la complexité des données médicales. Parmi ces défis figurent leur caractère implicite (dont l’interprétation reste difficile sans expertise médicale), leurs imperfections telles que l’incohérence, l’incertitude et l’incomplétude, ainsi que leur dimension temporelle intrinsèque. Cette thèse explore comment des approches fondées sur la logique peuvent remédier à ces difficultés.
    Dans un premier temps, j’ai étudié une approche ontologique afin d’illustrer l’apport des ontologies dans l’évaluation de la qualité des données médicales, en particulier pour le phénotypage des cancers du poumon. Cette approche a consisté à concevoir une ontologie pour formaliser les connaissances essentielles du domaine et l’exploiter pour interroger l’entrepôt de données de santé du CHU de Bordeaux. Ce travail a permis de mettre en évidence les apports des ontologies pour la représentation des connaissances et la détection d’incohérences, tout en soulignant certaines limites, notamment en ce qui concerne la gestion des incohérences temporelles dans les données de santé.
    Fort de cette première expérimentation, j’ai ensuite proposé un nouveau framework logique pour l’inférence d’événements cliniques de haut niveau à partir de données temporelles, en cohérence avec le raisonnement et la prise de décision cliniques. Ce framework définit des règles logiques exprimant les conditions d’existence d’un événement à un instant donné, ainsi que, de façon optionnelle, des conditions de terminaison signalant sa fin potentielle. Deux méthodes d’agrégation permettent ensuite de construire des intervalles d’événements à partir de ces conditions. Le formalisme introduit également la notion de méta-événements, obtenus par combinaison ou généralisation d’autres événements, et intègre des niveaux de confiance ainsi qu’un mécanisme de réparation pour traiter les imperfections inhérentes à la détection des événements. Pour valider l’intérêt de ce framework, j’ai implémenté ses composants principaux en Answer Set Programming. Le système obtenu, CASPER, a été évalué sur deux cas d’usage médicaux, démontrant à la fois sa faisabilité computationnelle et sa concordance avec l’avis d’experts médicaux.
     

    Amphi LaBRI