Agenda

Département
Langue
Date
Thématique
2025

November

  • 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

    English
    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.

    English
    LaBRI, salle 178
  • 16:00
    18:00

    To meet the exascale challenge, parallel programming models tend to abstract the machine details with task-based programming or by exposing the hardware at the software level (network with RDMA capabilities) with the Partitioned Global Address Space (PGAS) model. The Message Passing Interface (MPI) standard proposes a similar communication model to the PGAS model, via the MPI One-Sided Communications. These operations allow a better overlap of communications by computations compared to classic two-sided communications. However, programmers must handle data consistency and synchronisation to prevent data races, which can be a challenging task. Our study proposes two solutions to facilitate the use of one-sided communications in MPI progams. The first is to improve an existing data race detection tool to make it more scalable. The second is a tool that automatically transform two-sided communications into one-sided communications.

    English
    Amphi LaBRI
  • 09:30
    10:30

    Libraries of machine checked code are, nowadays, organized around hierarchies of algebraic structures. Unfortunately the language of Type Theory and the features provided by the Coq system make the construction of a hierarchy hard even for expert users. The difficulty begins with the non-orthogonal choices, between storing information as record fields or parameters, and between using type classes and canonical structures for inference. To this, one may add the concerns about performance and about the usability, by a non expert, of the final hierarchy.

    HB gives the library designer a language to describe the building blocks of algebraic structures and to assemble them into a hierarchy. Similarly it provides the final user linguistic constructs to build instances (examples) of structures and to teach the elaborator of Coq how to take advantage of this knowledge during type inference. Finally HB lets the library designer improve the usability of his library by providing alternative interfaces to the primitive ones, a feature that can also be used to accommodate changes to the hierarchy without breaking user code.

    This is a joint work with Kazuhiko Sakaguchi, Pierre Roux and Enrico Tassi
     

    Salle 76

December

  • 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

    English
    LaBRI 178
  • 15:30
    18:30

    Clément Gaspard will defend his thesis on December 8, 2025, at 3:30 p.m., in Lecture Hall 2 of Building 2A at the Bordeaux University Institute of Technology (Gradignan).
    The title of his thesis is: “Locomotion, step planning, and fall resistance in humanoid robots via reinforcement learning policies.”

     

    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

    English
    Amphi 2 Bat A IUT Gradignan
  • 14:00
    17:00

    The adoption of electronic health records has considerably enhanced access to large volumes of clinical data. While this accessibility is invaluable for both healthcare delivery and research, it also introduces new challenges arising from the complexity of medical data. These challenges include its implicitness (i.e., the need for domain expertise to interpret data), imperfections such as inconsistency, uncertainty, and incompleteness , and its inherently temporal nature. This thesis investigates how logic-based approaches can address these challenges.
    First, I investigated an ontology-driven approach to illustrate how ontologies can be used to evaluate medical data quality, with a focus on lung cancer phenotyping. This involved designing an ontology to capture essential domain knowledge and applying it to query the Clinical Data Warehouse of Bordeaux University Hospital. The work highlighted both the benefits of ontologies in representing domain knowledge and identifying inconsistencies, as well as their limitations, particularly in handling temporally inconsistent healthcare data.
    Building on this experience, I then proposed a novel logic-based framework for inferring high-level events from temporal clinical data, in a way that better aligns with clinical reasoning and decision-making . The framework defines logical rules specifying the existence conditions of an event at a given time-point, along with optional termination conditions that signal its possible end. It also introduces two aggregation methods to construct event intervals from these conditions. Furthermore, the formalism supports the definition of meta-events, obtained by combining or generalizing other events, and integrates confidence levels and a repair mechanism to handle imperfections in event detection. To validate the framework, I implemented its core components using Answer Set Programming, a declarative logic programming paradigm, and evaluated the resulting system, CASPER, on two medical use cases. The evaluation showed both computational feasibility and alignment with expert medical opinions.

     

    Amphi LaBRI