Schița subiectului
Liste des stages 2022-2023
Titre : Adaptation de résultats sur les graphes arbitrairement partitionnables (AP) aux graphes arbitrairement partitionnables à la volée et aux graphes récursivement arbitrairement partitionnables.
Encadrants : Olivier Baudon (olivier.baudon@labri.fr) et Julien Bensmail (Julien.BENSMAIL@univ-cotedazur.fr)
Résumé : Un graphe arbitrairement partitionable (en abrégé AP) est un graphe G simple à n sommets tel que pour toute suite (k1, ... ki) d'entiers dont la somme vaut n, il est possible de trouver une partition V1, ... Vi des sommets de G telle que pour tout i :
- l'ensemble Vi contient ki sommets
- le sous-graphe induit par Vi est connexe.
2 versions plus fortes de ce problème ont été ensuite proposées :- Un graphe G = (V, E) à n sommets est arbitrairement partitionable à
la volée (en abrégé OLAP) si et seulement si pour tout entier k <= n,
- soit n = k et G est connexe,
- soit il existe un sous-ensemble S de V de taille k tel que le sous-graphe induit par S soit connexe et le sous-graphe induit par V\S soit OLAP
- Un graphe G = (V, E) à n sommets est récursivement arbitrairement partitionable (en abrégé RAP) si et seulement si pour tout entier k <= n,
- soit n = k et G est connexe,
- soit il existe un sous-ensemble S de V de taille k tel que le sous-graphe induit par S soit RAP et le sous-graphe induit par V\S soit RAP.
Tout graphe RAP est OLAP et tout graphe OLAP est AP.
En 2020, Julien Bensmail a publié deux articles sur les graphes AP, un sur les graphes AP minimaux (toute suppression d'arête fait perdre la propriété d'être AP), un sur les valeurs du paramètre sigma3 (pour tout triplet de sommets u, v, w ne partageant aucune arête, nombre de sommets voisins d'au moins un des sommets u, v, ou w et non voisin des trois à la fois) impliquant que le graphe soit AP.
L'objectif de ce stage est d'adapter ces résultats aux graphes OLAP et RAP.Titre : Fun(gi) with codons. À quelles règles obéit l’organisation des codons ?
Encadrants : Patricia Thébault (patricia.thebault@u-bordeaux.fr), Raluca Uricaru (raluca.uricaru@u-bordeaux.fr) et Karine Dementhon (Laboratoire Microbiologie Fondamentale et Pathogénicité, Université de Bordeaux)
Résumé : La description est disponible ici.
Titre : Comparaison et complémentarité des approches par les données et par les modèles dans la cadre de la caractérisation d’un système technologique. Développement d’un cas illustratif
Encadrants : Bruno Pinaud (bruno.pinaud@u-bordeaux.fr) et Bruno Vallespir (bruno.vallespir@u-bordeaux.fr)
Résumé : La description est disponible ici.
Titre : Interruptions en espace utilisateur pour le réseau BXI
Encadrants : Alexandre Denis (Alexandre.Denis@inria.fr) et Grégoire Pichon (Gregoire.Pichon@atos.net)
Résumé : La description est disponible ici.
Titre : Conception d’outils pour la collaboration lors de travaux pratiques en réalité virtuelle
Encadrants : Arnaud Prouzeau (arnaud.prouzeau@inria.fr)
Résumé : La description est disponible ici.
Titre : Reasoning with hard and soft constraints to repair and query inconsistent data
Encadrants : Meghyn Bienvenu (meghyn.bienvenu@labri.fr) et Camille Bourgaux (camille.bourgaux@ens.fr)
Résumé : La description est disponible ici.
Titre : Classification supervisée et non supervisée des comptes rendus des appels au centre 15/SAMU de la Gironde par des réseaux de neurones de type Transformer : Application à la surveillance épidémiologique
Encadrants : Marta Avalos (marta.avalos-fernandez@inria.fr) et Emmanuel Lagarde (emmanuel.lagarde@u-bordeaux.fr)
Résumé : La description est disponible ici.
Titre : Autour des Graphes Universels Isométriques
Encadrants : Cyril Gavoille et François Dross
Résumé : La description est disponible ici.
Titre : Mesure et analyse du réseau Tor
Encadrants : Joachim Bruneau-Queyreix, Stéphane Delbruel, Laurent Réveillère
Résumé : La description est disponible ici.
Titre : Count-min-sketch collaboratifs pour la construction de systèmes distribués résilients aux attaques byzantines
Encadrants : Joachim Bruneau-Queyreix, Laurent Réveillère
Résumé : La description est disponible ici.
Titre : Calcul d’interactions sur GPU par une méthode hiérarchique
Encadrants : Olivier Coulaud (olivier.coulaud@inria.fr), Bérenger Bramas (berenger.bramas@inria.fr)
Résumé : La description est disponible ici.
Titre : Diff de code avec RWS-Diff
Encadrants : Jean-Rémy Falleri (falleri@labri.fr).
Résumé : La description est disponible ici.
Titre : Généralisation des permutations planes en 3D
Encadrants : Nicolas Bonichon (nicolas.bonichon@u-bordeaux.fr) et Philippe Duchon (philippe.duchon@u-bordeaux.fr)
Résumé : La description est disponible ici.
Titre : Energie ou performance : impact de l’implémentation sur la consommation
Encadrants : Amina Guermouche (Amina.Guermouche@inria.fr) et Abdou Guermouche (Abdou.Guermouche@u-bordeaux.fr)
Résumé : La description est disponible ici.
Titre : Interactive image colorization
Encadrants : Hernan Carrillo (hernan.carrillo-lindado@u-bordeaux.fr), Aurélie Bugeau (aurelie.bugeau@labri.fr ), Michaël Clément (michael.clement@labri.fr )
Résumé : La description est disponible ici.
Titre : Comprendre les relations entre les usages et les impact environnementaux du réseau internet via une modélisation probaliste basée capacité
Encadrants : Gaël Guennebaud (gael.guennebaud@inria.fr), Aurélie Bugeau (aurelie.bugeau@labri.fr )
Résumé : la description est disponible ici.
Titre : Modélisation des impacts environnementaux d'actions limitatives du streaming vidéo
Encadrants : Gaël Guennebaud (gael.guennebaud@inria.fr), Aurélie Bugeau (aurelie.bugeau@labri.fr )
Résumé : la description est disponible ici.
Titre : Services intelligents pour de l’edge computing
Encadrants : Stéphane Delbruel (stephane.delbruel@labri.fr), Joachim Bruneau-Queyreix (joachim.bruneau-queyreix@labri.fr)
Résumé : la description est disponible ici.
Titre : Arguments de terminaison avec l’assistant de preuve COQ (WQO with COQ)
Encadrants : Thibault Hilaire (thibault.hilaire@labri.fr), David Ilcinkas (david.ilcinkas@labri.fr) et Jerome Leroux (jerome.leroux@labri.fr)
Résumé : La preuve de terminaison d’algorithmes est un problème difficile. En effet, il faut montrer que les boucles s’arrêtent, c’est-à-dire qu'elles ne peuvent pas s’exécuter un nombre infini de fois. Pour montrer cela formellement, on peut utiliser une fonction vers les entiers naturels qui décroît strictement à chaque itération, ou bien plus généralement une fonction vers un ordre bien fondé qui décroît de même à chaque itération.
Pour certains algorithmes, ces ordres bien fondés proviennent de structures mathématiques appelées beaux préordres. Formellement un préordre est beau si de toute suite infinie d’éléments il est possible d’extraire une sous-suite croissante. Les beaux préordres peuvent se combiner, par exemple par produit cartésien, ou par extension à des mots. Les théorèmes montrant ses résultats sont appelés Lemme de Dickson et Lemme de Higman.
On souhaite pouvoir utiliser ces lemmes pour montrer formellement la terminaison de certains algorithmes à l’aide d’assistants de preuve, et en particulier avec l’outil COQ. Pour cela, les preuves des lemmes de Dickson et de Higman mais aussi la définition des beaux préordres, habituellement données en logique classique, doivent être converties en logique intuitionniste.
En 2012, Dimitrios Vytiniotis, Thierry Coquand et David Wahlstedt ont donné une définition en logique intuitionniste des beaux préodres, appelés relations presque pleines, et donnés une preuve du lemme de Dickson.
Il existe une autre façon de décrire les beaux préordres. L’objectif du stage est d’étendre les travaux sur les relations presque pleines à cette autre description, ou d’étendre le Lemme de Higman aux relations presques pleines. Dans tous les cas, on commencera par une preuve papier détaillée avant de l’implémenter dans l’outil COQ.
Mots-clés : Beaux préordres (well-quasi order), Lemme de Dickson, Lemme de Higman, Relations presque pleines (Almost-full relations), Assistant de preuve, COQ.
Bibliographie :
https://link.springer.com/chapter/10.1007/978-3-642-32347-8_17
https://fr.wikipedia.org/wiki/Lemme_de_Dickson
https://fr.wikipedia.org/wiki/Lemme_de_Higman
Titre : Support d’exécution à base de tâches et programmation de haut niveau pour la simulation par éléments finis
Encadrants : Olivier Aumage (olivier.aumage@u-bordeaux.fr)
Résumé : la description est disponible ici.
Titre : Abstraction de la vectorisation pour les nouvelles architectures matérielles
Encadrants : Raphael Gayno, Olivier Aumage (olivier.aumage@inria.fr), Adrien Cassagne
Résumé : la description est disponible ici.
Titre : Développement logiciel d'un plugin dans medInria dans le contexte de la recherche
Encadrants : Julien Castelneau (julien.castelneau@inria.fr), François Rue et Florent Leray
Résumé : la description est disponible ici.
Titre : Développement logiciel d'un plugin dans medInria dans le contexte de la recherche
Encadrants : Julien Castelneau (julien.castelneau@inria.fr), François Rue et Florent Leray
Résumé : la description est disponible ici.
Titre : I.A. de Confiance : Encadrement de Décisions issues De l’Apprentissage Automatique par des Preuves Formelles
Encadrants : Laurent Simon (lsimon@labri.fr)
Résumé : la description est disponible ici.
Titre : Apprentissage de systèmes I.A. de confiance, une approche neuro-symbolique
Encadrants : Laurent Simon (lsimon@labri.fr)
Résumé : la description est disponible ici.
Titre : Apprentissage par Renforcement / Mécanismes d’Attention pour la résolution pratique de SAT
Encadrants : Laurent Simon (lsimon@labri.fr)
Résumé : la description est disponible ici.
Titre : Algorithmes distribués pour les réseaux de capteurs sans fil à récupération d'énergie
Encadrants : Nicolas Hanusse (nicolas.hanusse@labri.fr)
Résumé : Les réseaux de capteurs ont de nombreuses applications, notamment la surveillance de l'environnement à grande échelle (qualité de l'air, de l'eau, suivi des plantes/animaux, surveillance des catastrophes, etc.) Ces systèmes sont constitués de dispositifs répartis dans l'environnement, dotés de capacités de communication sans fil à portée limitée et d'une certaine puissance de calcul et de détection. Les nœuds de capteurs sont généralement alimentés par des piles, ce qui limite la durée de vie du système ou nécessite des opérations de maintenance complexes, voire pas toujours réalisables, pour recharger ou remplacer les piles.
Pour remédier à ces inconvénients, de nouveaux capteurs capables de récolter de l'énergie de leur environnement ont été développés. Par exemple, ces capteurs peuvent s'appuyer sur les radiations solaires ou autres radiations électromagnétiques, les flux d'air ou d'eau, les mouvements, les gradients de température, etc. pour collecter de l'énergie [1]. Bien qu'un grand nombre de recherches soient consacrées à la minimisation de la consommation d'énergie dans le cas des capteurs alimentés par batterie, les capacités de récupération d'énergie posent de nouveaux défis dans la conception et l'évaluation des protocoles pour les réseaux de capteurs sans fil. En effet, un nœud peut être temporairement déconnecté lors de la recharge de sa batterie, l'énergie disponible peut varier dans le temps (par exemple, le rayonnement solaire disponible dépend de la météo et de l'heure actuelle). Par conséquent, les approches traditionnelles telles que l'alternance à une fréquence fixe entre le mode veille et le mode sommeil ne fonctionnent pas ou entraînent une latence élevée. Une tâche classique dans les réseaux de capteurs consiste à agréger les données du nœud vers un ou plusieurs nœuds désignés, appelés stations de base. Ces nœuds spéciaux peuvent être capables de communiquer avec une autre entité en dehors du réseau de capteurs, ou de prendre des mesures si les capteurs signalent une anomalie dans l'environnement. Les solutions actuelles pour les réseaux de capteurs alimentés par batterie reposent souvent sur un réseau superposé le long duquel les données sont agrégées et propagées vers les stations de base et/ou sur des horaires fixes spécifiant quand un nœud doit transmettre. Un des objectifs de ce stage est de revisiter l'agrégation de données dans le contexte des réseaux de capteurs à récupération d'énergie. On peut commencer par lire [2]. Une question plus large est de déterminer à quel rythme et/ou avec quelle couverture de tels réseaux peuvent traiter des données tout en maintenant le niveau d'énergie d'un nombre suffisant de nœuds suffisamment élevé pour l'agrégation et le rapport aux stations de base.
Références bibliographiques :
[1] Energy-Harvesting Wireless Sensor Networks (EH-WSNs): A Review Kofi Sarpong Adu-Manu, Nadir Adam, Cristiano Tapparello, Hoda Ayatollahi, and Wendi Heinzelman, ACM Transactions on Sensor Networks (TOSN) 2018
[2] Energy-Collision Aware Data Aggregation Scheduling for Energy Harvesting Sensor Networks. Quan Chen, Hong Gao, Zhipeng Cai, Lianglun Cheng and Jianzhong Li. Infocom 2018
Les stages de l'équipe projet Inria Manao sont disponible ici.Titre : Diffusion models for image colorization
Encadrants : Rémi Giraud (remi.giraud@u-bordeaux.fr) et Michaël Clément (michael.clement@labri.fr)
Résumé : la description est disponible ici.
Titre : Sécurité des communications orientée couche physique
Encadrants : Stéphane Delbruel (stephane.delbruel@labri.fr) et Joachim Bruneaux-Queyreix (joachim.bruneau-queyreix@u-bordeaux.fr)
Résumé : la description est disponible ici.
Titre : Intégration de capacités de calcul quantique dans un support d’exécution à base de tâches
Encadrants : Olivier Aumage (olivier.aumage@inria.fr)
Résumé : la description est disponible ici.
Titre : Parallélisation et équilibrage de chaînes de traitement de signal pour la radio-astronomie
Encadrants : Olivier Aumage (olivier.aumage@inria.fr)
Résumé : la description est disponible ici.
Titre : Deep Learning for Multisite MRI Harmonization
Encadrants : Pierrick Coupé (pierrick.coupe@labri.fr)
Résumé : la description est disponible ici.
Autres offres de stage (2022-2023)
Stages à coloration recherche proposés par la SNCF