Agenda

Département
Langue
Date
Thématique
2025

novembre

  • 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
  • 14:00
    15:00

    Aditya Prakash
    Resolving nondeterminism in automata

    In this talk, we will look at automata where nondeterminism can be resolved on-the-fly, such that this resolution constructs accepting runs on accepting words. The automata where this is possible are called history deterministic automata. We will look at the complexity and algorithms for the problem of recognising history-deterministic automata. We will also look at automata where the resolution of nondeterminism can be done by a stochastic policy. I will end the talk with my currently favourite conjecture on such automata, which, if true, would have an elegant implication for population games.

    Français
    178

décembre

  • 11:00
    12:00

    Mouna Safir (ENS Lyon)

    Title: Self-Stabilizing Mutual Exclusion in Dynamic Networks with Bounded Temporal Diameter

    Abstract:

    We consider distributed systems subject to frequent topological changes. Specifically, we assume the network topology evolves as a dynamic graph in which, at any point in time, the temporal distance between any two processes is at most Δ.

    In this setting, where processes have unique identifiers and know both Δ and an upper bound N on the system size n, we introduce a self-stabilizing solution to the mutual exclusion problem.

    Our algorithm stabilizes in O(NΔ) rounds, uses bounded memory, and once converged guarantees an optimal waiting time of n−1 rounds before a process can enter its critical section.

    The solution is built from three self-stabilizing algorithms: Leader Election, Unison, and Ranking. We contribute new self-stabilizing algorithms for Unison and Ranking, and we combine them with a recent leader election protocol from Altisen et al. (TCS 2023).

    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
  • 15:30
    18: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)
  • 15:30
    16:30

    Locomotion, step planning, and fall resistance in humanoid robots via reinforcement learning policies

    Français
    Amphi 2 Bat A IUT Gradignan
  • 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