ED Mathématiques et Informatique
COVERABILITY ALGORITHMS FOR PETRI NETS CERTIFIED IN COQ
by Thibault HILAIRE (LaBRI - Laboratoire Bordelais de Recherche en Informatique)
The defense will take place at 14h00 - 050-AMPHI 351, cours de la Libération F-33405 Talence cedex
in front of the jury composed of
- Jérôme LEROUX - Directeur de recherche - CNRS,Université de Bordeaux - Directeur de these
- Serge HADDAD - Professeur émérite - École normale supérieure Paris-Saclay (ENS Paris-Saclay) - Rapporteur
- David ILCINKAS - Chargé de recherche - CNRS,Université de Bordeaux - CoDirecteur de these
- Frédéric BLANQUI - Directeur de recherche - École normale supérieure Paris-Saclay (ENS Paris-Saclay) - Rapporteur
- Anca MUSCHOLL - Professeure des universités - Université de Bordeaux - Examinateur
- Laure PETRUCCI - Professeure des universités - CNRS,Université Paris 13 - Examinateur
In recent years, concurrent systems have become an increasingly common feature of modern IT systems, especially mission-critical systems. However, checking that they behave correctly is no easy task. That's why in this thesis we focus on formal verification, and more specifically on model-checking. Petri nets are a well-studied and well-known model for verifying concurrent systems. The computation of the coverability set is one of the most fundamental problems concerning Petri nets, and it is the one that interests us in this thesis. However, certain behaviors in coverability set computation algorithms can give rise to subtle and hard-to-find bugs. That's why we've turned our attention to proof assistants, and in particular to Coq. Using it, we certified the correction and termination of the MinCov algorithm by Finkel, Haddad and Khmelnitsky (FOSSACS 2020). This algorithm is the most recent in the literature to calculate the minimum basis of the coverability set. In addition to the intrinsic interest of a computer-verified proof, our certification provides AbstractMinCov, a small-step variant of MinCov. The introduction of this new algorithm opens the way to a better understanding of the general problem, as well as possibilities for future optimizations.
ED Sciences Chimiques
Solid state NMR studies of functionnal amyloids
by Loïc DELCOURTE (Institut de Chimie & de Biologie des Membranes & des Nano-objets)
The defense will take place at 14h00 - Auditorium IECB 2 rue Robert Escarpit 33600 Pessac
in front of the jury composed of
- Antoine LOQUET - Directeur de recherche - Université de Bordeaux, CBMN - Directeur de these
- Roland RIEK - Professeur - ETH Zurich - Rapporteur
- Miguel MOMPEAN - Directeur de recherche - Instituto de Química-Física Rocasolano - Rapporteur
- Marie-France GIRAUD - Chargée de recherche - Université de Bordeaux, CBMN - Examinateur
- Anja BOCKMANN - Directrice de recherche - Université de Lyon, IBCP - Examinateur
- Sven SAUPE - Directeur de recherche - Université de Bordeaux, IBGC - Examinateur
Signalosomes are higher-order biomolecular assemblies involved in signaling process from innate immunity, and which activation and formation leads to a unique type of regulated cell death called necroptosis. Also coined inflammasomes, resistosomes or necrosomes, they are essential for fighting off infections and pathogens. Signalosomes are particularly associated with Nucleotide-binding Leucine-Rich repeat (NLR) proteins, as ubiquitous class of cytosolic receptor proteins. In eukaryotes, NLR assemble in wheel-like structures that can act as ion channels, membrane-pores or molecular scaffold for the assembly of downstream effectors. A trend that has emerged in fungi and animals is the use of short functional amyloid motifs for signal transduction. Prime examples of this are the Prion Forming Domains (PFD) from Podospora anserina and the RIP Homotypic Interaction Motifs (RHIM) from mammals, that both allow for signal transmission from protein to protein. Until recently, it was not known if prokaryotes possessed signalosome-like architectures capable of triggering cell-death in response to non-self-recognition. While bacterial amyloids are involved in the formation of biofilm, very little was known about other uses bacteria have for this unique class of proteins. Bioinformatic studies revealed the existence of set of genes similar to fungal signalosomes in filamentous, multicellular colonial bacteria. Short amino-acids motifs with predicted amyloid propensity were termed BASS for Bacterial Amyloid Signaling Sequences, and were identified in both cell-death executor-like proteins and NLRs. Our study set out with the aim of deciphering the structure and assembly mechanism of these hypothetical bacterial signalosomes. We focused on the protein B2-B from Streptomyces Olivochromogenes, composed of a N-terminal putative cell-death effector BELL domain and a C-terminal BASS domain. Our divide-and-conquer approach allowed us to efficiently use solution NMR, solid-state NMR, X-ray crystallography and other biophysical methods to unravel their structures, BASS assembly mechanisms, establish a cross-kingdom analysis of signalosome formation and signalosome-related amyloids, and make new hypotheses about the evolutionary relationships of amyloid-mediated cell-death mechanisms throughout the tree of life.
ED Sciences de la Vie et de la Santé
The implication of annexins in the development of human muscular dystrophies
by Léna D'AGATA (Institut de Chimie & de Biologie des Membranes & des Nano-objets)
The defense will take place at 13h30 - Amphithéâtre du bâtiment B6 Avenue des Facultés 33600 Pessac
in front of the jury composed of
- Benoît ARVEILER - Professeur des universités - praticien hospitalier - Université de Bordeaux - Examinateur
- Marie-Laure MARTIN-NéGRIER - Professeur des universités - praticien hospitalier - Université de Bordeaux - Examinateur
- Bénédicte CHAZAUD - Directrice de recherche - Inserm - Rapporteur
- Catherine COIRAULT - Directeur de recherche - Inserm - Rapporteur
Sarcolemma (micro-)disruption is a physiological phenomenon induced by mechanical stress in muscle fibers. Normal skeletal muscle cells are able to repair these ruptures at the minute scale. According to current models of cell membrane repair, membrane resealing is an active Ca2+-dependent process based on the formation of a membrane patch by aggregation of intracellular vesicles and fusion of the patch with the cell membrane surrounding the disruption site. The molecular machinery start being identified, with notably dysferlin, caveolin-3, MG53, AHNAK or Annexins (ANX). The group of A. Bouter has shown that ANXA5 (Carmeille et al., 2016 et 2017) and ANXA6 (Croissant et al., 2020) are instrumental for the membrane repair of human skeletal muscle cells. Whereas a normal cell is able to reseal rapidly a membrane disruption, defective membrane repair leads to cell death and may contribute to the development of degenerative diseases, such as muscular dystrophies. Limb girdle muscular dystrophy type (LGMD) R2 and Miyoshi myopathy result from a defect of membrane repair. Some other myopathies may also result from a defect in the membrane repair machinery. In addition, it has been reported that the same primary mutation results in variable disease progression due to the existence of secondary genetic variants, termed genetic modifiers, which greatly impact the severity of the muscular dystrophy. In this context, it has been shown that ANX are often dysregulated in many muscular dystrophies. The PhD thesis aimed at addressing the interplay of muscular dystrophies and membrane repair. From skeletal muscle cells collected from patients suffering from LGMDR2, rippling muscle disease, facioscapulohumeral muscular dystrophy or Duchenne muscular dystrophy, I identified those exhibiting a defect of membrane repair. I also measured expression level and subcellular distribution of main components of the membrane repair machinery in these cells. Finally, I initiated work aiming at studying the involvement of helping cells (macrophages and fibro-adipogenic precursors) in sarcolemma repair. This work contributes to providing fundamental knowledge to guide future therapeutic strategies. The existence of a correlation between ANX and clinical severity of muscular dystrophies could also serve as a prognostic indicator of the disease.
New therapeutic strategies in the treatment of diffuse intrinsic pontine glioma
by Guillaume HERRAULT (BoRdeaux Institute of onCology)
The defense will take place at 14h00 - Amphithéatre Bâtiment Bâtiment "Bordeaux Biologie Santé" 2 Rue Dr Hoffmann Martinot, 33000 Bordeaux
in front of the jury composed of
- Nicolas LARMONIER - Professeur des universités - Université de Bordeaux - Examinateur
- Eddy PASQUIER - Directeur de recherche - Aix Marseille Université - Rapporteur
- Isabelle PELLIER - Professeure des universités - praticienne hospitalière - Université d'Angers - Rapporteur
- Christophe GROSSET - Directeur de recherche - Université de Bordeaux - Directeur de these
Diffuse intrinsic pontine glioma (DIPG) is a pediatric cancer representing 80% of all brainstem pediatric tumors. This type of cancer has a very poor prognosis, with an average survival of 8 to 12 months. It is notably characterized by mutations in the genes encoding histone H3, resulting in the substitution of lysine 27 with methionine (H3K27M). Over the past thirty years, no significant improvement in survival has been observed for children with DIPG. The aim of this thesis is therefore to propose new therapeutic strategies for the treatment of DIPG by utilizing various in vitro and in vivo models. A pharmacological screening on a spheroid model was conducted, revealing a therapeutic target that has been little described in these tumors. A kinomic analysis revealed that the use of this compound led to the activation of an important kinase. The combination of inhibitors targeting these two pathways showed a promising synergistic effect for treating DIPG. Additionally, the molecular analysis of the effects of a combination discovered in the laboratory, involving GSK126, an inhibitor of EZH2 methyltransferase activity, in combination with statins, has highlighted new therapeutic targets of interest.
Neuronal basis of decision-making under opposed valence affectivestates
by Anass EL AZRAOUI (Institut Interdisciplinaire de Neurosciences)
The defense will take place at 14h00 - Salle de conférence Salle de conférence, CGFB 146 rue Léo saignat, Bordeaux, 33000
in front of the jury composed of
- Yann HUMEAU - Directeur de recherche - Université de Bordeaux - Directeur de these
- Daniel SALZMAN - Full professor - University of Columbia - Rapporteur
- Andreas LUTHI - Full professor - Friedrich Miescher Institute for Biomedical Research - Rapporteur
- SHAUNA PARKES - Chargée de recherche - INCIA, CNRS-Université de Bordeaux - Examinateur
- STEPHANIE TROUCHE - Chargée de recherche - IGF, CNRS - Examinateur
The emotional impact of a stimulus or an environment shapes decision-making and drives adaptive behaviors. However, when emotional values are altered by mood disorders or diseases like pathological anxiety or post-traumatic stress disorder, this can lead to inappropriate or maladaptive behaviors. The prefrontal cortex (PFC) is among the brain regions altered in such pathologies, with its ventral sub-division known to regulate emotions and its dorsal sub-division involved in decision-making and executive functions. These data point to the PFC as a key region for the modulation of goal-directed behaviors, however, a circuit-based understanding for how PFC encodes emotional value and integrates it into decision-making processes remains elusive. To address this question, we used Neuropixels recordings in PFC circuits while mice performed a virtual-reality based decision-making task in which they are trained to approach a visual stimulus rewarded in one context, but avoid the same stimulus when it is punished in a second context. The context thus determines the current emotional value of a primary visual stimulus, and decisions about the same stimulus are made accordingly. Our recordings indicate that different populations of PFC neurons are activated by different emotional contexts, and that the same behavioral choices, are driven by different PFC circuit dynamics as a function of the emotional context. These data suggest a dynamical encoding of goal-directed behaviors unfolded within prefrontal circuits.
ED Sciences et environnements
Towards pesticide-free viticulture: analysing the microbiome of grapevines and vineyard soils to develop microbial biocontrol of downy mildew
by Paola FOURNIER (BIOGECO - BIOdiversité, Gènes & Communautés)
The defense will take place at 9h30 - Amphithéâtre Colette et Josy Bové 71 avenue Edouard Bourlaux - CS 20032 - Amphithéâtre Colette et Josy Bové - 33882 VILLENAVE-D'ORNON CEDEX - INRA Bordeaux
in front of the jury composed of
- Corinne VACHER - Directeur de recherche - INRAE - Directeur de these
- Cendrine MONY - Professeur - Université de Rennes 1 - Rapporteur
- Alain SARNIGUET - Directeur de recherche - IRHS - Rapporteur
- Pierre-Emmanuel COURTY - Directrice de recherche - INRAE - Examinateur
- Stéphanie CLUZET - Professeur - Université de Bordeaux - Examinateur
- Adrian MARIELLE - Professeur - Université de Bourgogne - Examinateur
- Patrice THIS - Directeur de recherche - INRAE - CoDirecteur de these
Grapevines and viticultural soils host a great diversity of microorganisms that collectively form the microbiota. Some microorganisms are pathogens, such as the oomycete Plasmopara viticola, which causes downy mildew. Others, such as growth promoters and pathogen antagonists, are beneficial to grapevine health. These plant-microbe and microbe-microbe interactions have received increased attention in recent years because understanding them could provide a way to reduce the use of pesticides. The VITAE research programme (2020-26) combines several innovative management approaches to reduce fungicide use in viticulture. One of these approaches is the management of vine microbiota and vineyard soils to control foliar diseases, including downy mildew. The aim of this thesis is to identify microorganisms, whether bacteria or fungi, that may contribute to the biocontrol of downy mildew. The first chapter is a literature review on the dynamics of interactions between the vine and its microbiota throughout the evolutionary history and life of the plant. The second chapter compares the microbiota of asymptomatic leaf tissues with the microbiota associated with downy mildew lesions. It shows that downy mildew lesions harbor basidiomycete yeasts (Sporobolomyces patagonicus, S. roseus, Cryptococcus laurentii, and Udeniomyces pyricola) and bacteria (Bacillales, Streptomycetales), most of which are known for their biocontrol properties. In contrast, asymptomatic leaf tissues are more associated with other aerial pathogens (powdery mildew, Botrytis). These results suggest that the leaf locally recruits certain microbial taxa with biocontrol activity during downy mildew infection. The third chapter analyses the leaf and surface soil microbiota in plots selected on the basis of epidemiological surveys. It shows that certain fungal microbial taxa (for example, Buckleyzyma aurantiaca, Bullera alba, Trichoderma virens, and Trichoderma hamatum) and bacterial taxa (for example, the genera Streptomyces and Bacillus) are systematically more abundant in historically less downy mildew-susceptible plots. These taxa are abundant in the soil surface layer, where the oospores (the dormant form of the pathogen) overwinter, and in the phyllosphere, where the zoospores (flagellated spores, the form responsible for infection) infect the leaves. In contrast, the leaf endosphere, where the pathogen's mycelium develops, contains few microbial taxa linked to epidemiological data. This third chapter also shows that the composition of the surface soil microbiota allows for the prediction of a plot's susceptibility to downy mildew. The fourth chapter examines the role of leaf microbiota in downy mildew resistance of two American grapevine species (Vitis aestivalis and V. labrusca). This chapter is based on a sampling campaign carried out on the east coast of the United States. The data are currently being analysed. In conclusion, the thesis revealed the existence of microbial consortia naturally present in vineyards, which are promising candidates for the biocontrol of downy mildew. These microorganisms are present in the phyllosphere and in the surface soil at the beginning of the growing season and then seem to increase in abundance in the disease lesions. The main perspectives are: (i) the isolation of microbial candidates and the experimental evaluation of their biocontrol activity, either alone or combined in synthetic communities, (ii) the identification of agronomic practices that favour the identified microbial consortia, and (iii) the development of microbiota-based predictive tools for downy mildew susceptibility.
ED Sociétés, Politique, Santé Publique
Study of Multiple System Atrophy progression in the French cohort of the national reference centre: Longitudinal and multidimensional statistical approach
by Tiphaine SAULNIER (Bordeaux Population Health Research Center)
The defense will take place at 14h00 - amphithéâtre P.A. Louis 146 rue Léo Saignat, Bâtiment ISPED, Campus Carreire 33000 Bordeaux
in front of the jury composed of
- Cécile PROUST-LIMA - Directrice de recherche - Bordeaux Population Health - Directeur de these
- Véronique SéBILLE-RIVAIN - Professeure des universités - praticienne hospitalière - Nantes Université - Rapporteur
- Alexandra FOUBERT-SAMIER - Praticienne hospitalière - Institut des Maladies Neurodégénératives - CoDirecteur de these
- Caroline MOLLEVI - Ingénieure de recherche - CHU de Montpellier - Rapporteur
- Jean-Christophe CORVOL - Professeur des universités - praticien hospitalier - Sorbonne Université - Examinateur
- Antoine BARBIERI - Maître de conférences - Bordeaux Population Health - Examinateur
- Alexis ELBAZ - Directeur de recherche - INSERM, unité 1018 - Examinateur
Multiple System Atrophy (MSA) is a rare and incurable neurodegenerative disease, which progression remains poorly under-stood to date. Due to its low incidence, few epidemiological cohorts exist, and few studies are conducted on this pathology. As for many neurodegenerative diseases, the collected data are complex to analyze: they are often longitudinal, multidi-mensional, of various natures, and their observation process may be truncated by clinical events. This raises important methodological challenges that current statistical models do not yet fully tackle. This thesis focuses on the study of MSA progression through the development of statistical methods to fully exploit the lon-gitudinal data of the FMSA cohort, a prospective clinical cohort of patients diagnosed with MSA and followed in Bordeaux or Toulouse hospitals. This cohort has become one of the largest worldwide, with more than 650 patients, an observed follow-up duration up to 11 years, and a complete standardized annual follow-up including multiple measures of impairments and patient impressions, until patient's death. The epidemiological objectives of the thesis are to describe the evolution of MSA from two perspectives: from the patient, by studying the degradation in patient quality of life over the course of the disease, and from the clinician, by studying the progression of motor and non-motor impairments induced by MSA, and describing the natural history of the disease to establish the timeline of the various underlying mechanisms involved. The first part focuses on the development of JLPM (Joint Latent Process Model), a model designed to describe the progression over time of a latent construct, underlying one or multiple markers possibly of different natures. The model jointly evaluates the risk of events occurrence during follow-up to account for potential informative dropout. The second part introduces the 4S method, a four-step strategy for the longitudinal analysis of data derived from multidi-mensional measurement scales. The developed approach consists of successively structuring the scale into subdimensions (Structuring), describing the sequence of item impairments over time for each subdimension using a JLPM model (Sequenc-ing), aligning the evolution of each subdimension with disease progression (Staging), and identifying the most informative items (Selecting). The third part focuses on the development of LTSM (Latent Time Shift Model), a model designed to describe the progression of a disease according to its own disease timeline when it is not directly observed. Based on an individual recalibration of time, the model reconstitutes the disease timeline while describing the progression of multiple markers, offering an over-view of the evolution of impairments. The model also accounts for potential informative dropout. This thesis provides a more precise understanding of MSA progression through novel statistical methodologies that tackle the main analytical challenges. Through its findings, it highlights avenues for improving patient support and individual fol-low-up, as well as for designing clinical trials by targeting relevant disease markers for new therapeutic approaches. Beyond MSA, the biostatistical developments stemmed from this thesis are available as R packages, thereby providing accessible tools for studying other pathologies or even other applications facing similar methodological challenges.