Étudiants

L3

Jean-Gabriel Béchard, Léo Colisson, Félix De Framond, Rémi Desgranges, Johan Girardot, Émilie Grienenberger, Paul Jeanmaire, Jules Kozolinsky, Alexis Laouar, Gabriel Le Bouder, Kévin Le Run, Aliaume Lopez, Damien Mayaux, Noël Nadal, Simon Nivelle, Rémi Oudin, Pauline Pommeret, Xavier Poulot-Cazajous, Laurent Prosperi, Clémence Reda, Julien Rixte, Lucas Serrano, Arthur Talbot, Rébecca Zucchini.

M1

Emmanuel Arrighi, William Babonnaud, Louis Cohen, Xavier Erny, Rémy Garnier, Alexis Ghyselen, Arnaud Guerquin, Mathieu Hilaire, Mathieu Huot, Florent Koechlin, Théodore Lopez, Adina Nedelcu, Bogdan Ursu.

Le LORIA

Programme de la visite

Liste des ateliers proposés aux élèves

Jean-Yves Marion : Virologie

En 30 minutes, j'exposerai les différents défis actuels qui concernent les codes malveillants (virus, vers, botnet, ...). On verra que les questions pratiques soulèvent des questions plus fondamentales et théoriques.

Véronique Cortier : Vote électronique

Le vote électronique soulève de nombreux problèmes de recherche. Qu'est-ce qu'un bon système de vote électronique ? Est-ce réalisable ? Comment analyser un système de vote ? Nous aborderons ces questions au cours de l'exposé et nous montrerons comment les techniques d'analyse formelle développées dans l'équipe Cassis permettent d'étudier ces protocoles.

Mathieu Hoyrup : Lire un programme ou l'exécuter : quelle différence ?

Que peut-on savoir d'une fonction si elle nous est présentée :

• sous forme d'un programme calculant cette fonction,
• sous forme d'une boîte noire permettant de connaître les valeurs de cette fonction sur toutes les entrées.

Disposer d'un programme donne au moins autant d'information qu'avoir accès à la boîte noire. Cela donne-t-il plus d'information ? Dans ce cas, quel type d'information ? Cette question est un des problèmes les plus fondamentaux de l'informatique théorique et a donné lieu à de nombreux travaux, à commencer par ceux de Turing. Je présenterai les résultats historiques ainsi que les développements récents. Le domaine de recherche est la théorie de la calculabilité.

Paul Zimmermann : Casser RSA avec CADO-NFS

Le logiciel CADO-NFS implante l'algorithme du crible algébrique, qui a notamment été utilisé pour casser le challenge RSA-768. L'équipe Caramel a pour objectif de factoriser RSA-1024 avec CADO-NFS. Il reste à résoudre quelques défis pour y arriver...

Sylvain Lefebvre : Modélisation de structures complexes par l'exemple pour la fabrication additive

Nous nous intéressons à la génération automatique de structures complexes pour la fabrication additive (e.g. motifs entrelacés, treillis). Ces structures sont difficiles à créer manuellement car elles sont à la fois très détaillées mais doivent aussi respecter des contraintes mécaniques et géométriques strictes. Je présenterai plusieurs travaux récents qui permettent de générer automatiquement des telles structures à partir d'exemples.

Simon Perdrix : Informatique quantique

Des phénomènes mis en évidence par la physique quantique dans le comportement des particules élémentaires sont désormais considérés sous l'angle de leur exploitation pour représenter, traiter et communiquer l'information. Des résultats algorithmiques (algorithme de factorisation de Shor, algorithme de recherche de Grover), cryptographiques (distribution quantique de clés BB84, téléportation) et des avancées expérimentales soulignent l'intérêt d'un fondement quantique des sciences de l'information. Nous présenterons ce domaine de recherche notamment à travers les activités sur ce sujet de l'équipe Carte.

Jean-Baptiste Mouret : Des robots qui s'adaptent comme des animaux

Cet atelier sera composé d'un exposé (environ 45 minutes), suivi d'une visite de notre salle expérimentale robotique. L'exposé portera sur le sujet suivant. Après 50 ans de recherche en robotique, nous savons maintenant fabriquer des robots qui sont très efficaces pour des tâaches spécifiques et répétitives, mais on ne sait toujours pas comment les rendre capables d'opérer en dehors des environnements contrôlés des usines. C'est parce que les robots industriels et les robots pour le monde réel demandent des théories et des hypothèses fondamentalement différentes. Dans nos travaux, nous faisons l'hypothèse que les robots pour le monde réel doivent s'adapter comme des animaux : grâce à un processus d'apprentissage par essai-erreur guidé par de bonnes intuitions, qui sont elles-mêmes le résultat de milliards d'années d'évolution et d'années d'expérience. Nous décrirons nos derniers résultats qui permettent à un robot marcheur de s'adapter à des pannes non anticipée (e.g. la perte d'une patte) par essai-erreur en moins de 2 minutes. La visite portera sur les robots hexapodes de notre groupe ansi que sur l'infrastructure logicielle et matérielle utilisée dans les expériences.

Emmanuel Vincent et Slim Ouni : Traitement de la parole acoustique-visuelle et de la musique

Cet atelier se focalise sur deux défis de traitement des signaux audio et audiovisuels : la séparation de sources et la synthèese de la parole audiovisuelle. La séparation de sources vise à extraire le signal d'un locuteur ou d'un instrument de musique d'un enregistrement contenant d'autres sources sonores. Elle repose sur l'analyse temps-fréquence et l'apprentissage automatique et permet d'améliorer la qualité des communications téléphoniques et de la commande vocale ou de remixer la musique, entre autres applications. La synthèse de la parole audiovisuelle porte sur l'animation réaliste d'une tête parlante virtuelle (avatar) qui prend en compte les mécanismes d'articulation de la parole (les mouvements des lèvres, de la langue et de la mâchoire). Dans nos travaux, nous utilisons des outils de capture de mouvement pour le visage (techniques de stéréovision : avec et sans capteurs) et pour les mouvements des lèvres et de la langue (technique d'électromagnétographie). Ces données permettent de développer des algorithmes d'animation du visage synchrone avec la parole.

Steve Kremer : Vérification de protocoles cryptographiques

Les protocoles cryptographiques sont des programmes distribués qui utilisent des primitives cryptographiques, telles que le chiffrement, pour assurer des propriétés de sécurité, comme par exemple la confidentialité. Cependant, même sans casser la cryptographie, il est souvent possible de déjouer les objectifs de ces protocoles. Nous allons voir comment utiliser des outils issus de la logique pour trouver des failles, ou prouver leur absence, dans ces protocoles.

Jasmin Blanchette, Marie Duflot et Stephan Merz : Dompter des algorithmes avec de la logique

Nous étudions comment des techniques fondées sur la logique formelle peuvent aider à raisonner sur les algorithmes et systèmes informatiques, en particulier distribués. Différentes techniques interviennent, selon qu'il s'agisse de trouver des erreurs (model checking) ou de démontrer formellement la correction par des outils de preuve automatique ou interactive. Pour les plus grands systèmes, mais aussi pour étudier des aspects quantitatifs (temps de réponse, ressources en mémoire ou réseau), il est utile de combiner logique et statistiques. Nous allons présenter les bases de nos travaux, ainsi que des idées pour d'éventuels stages.

Dave Ritchie : The Capsid Team : Developing Computational Algorithms for Protein Structures and their Interactions

Capsid is a new research team at Inria Nancy / LORIA, which was created in 2015. The main aim of the team is to work on problems in structural biology. This work involves developing efficient ways to represent and compare large three-dimensional bio-molecules such as proteins. For example, if we have two different but related proteins, how can we measure how similar they are? If we know from biology that two or more proteins can fit together (or dock) to form a complex, how can we simulate this in a computer? In this workshop, I will talk about some of the problems that the Capsid team are working on, and I will demonstrate some of our software for comparing different protein structures and for docking two or more proteins to make models of large 3D protein complexes. The presentation will be in English.

Olivier Devillers et Monique Teillaud : L'ordinateur géomètre

Les membres du projet Vegas présenteront des démos autour de leur sujet de recherche.

• Dessiner des courbes sans confondre proximité et intersections
• Des géométries exotiques pour déplier le tore ou le double-tore
• Faire un compromis entre le cas le pire et le complétement aléatoire.

Pierrick Gaudry : Le logarithme discret, de la théorie des nombres à la sécurité d'Internet

Le problème du logarithme discret est au cœur de nombreux algorithmes utilisés pour sécuriser les communications. Le meilleur algorithme connu pour attaquer ce problème, le crible algébrique, doit être étudié en profondeur, aussi bien en théorie qu'en pratique afin de régler au mieux les paramètres des protocoles cryptographiques. Nous donnerons un aperçu du crible algébrique et raconterons comment une de ses particularités est à la base de la découverte récente d'une faille importante dans la mise en œuvre du protocole TLS.

Bruno Lévy : Simulation numéerique, lois de conservation et transport optimal

La simulation numérique permet de reproduire dans un ordinateur le comportement de différentes lois physiques, modélisées par des equations aux dérivées partielles. L'une des difficultés est de s'assurer que les lois de conservation soit bien respectées par ces simulations numériques. Dans certains cas, par exemple le problème de reconstruction de l'état de l'univers peu après le big-bang [1], l'expression de ces lois de conservation permet d'établir des relations intéressantes avec d'autres domaines des mathématiques, tels que la théorie du transport optimal [1,2]. En termes informatique, ceci conduit à de nouveaux schémas numériques, faisant appel à une forte composante géométrique [3,4].

1. Reconstruction of the early universe as a convex optimization problem, Brenier, Frisch et al., 2003, arXiv:astro-ph/0304214
2. Optimal Transport, Old and New, Villani, 2008
3. A multiscale approach to optimal transport, Mérigot, Symp. on Geometry Processing, 2011
4. A numerical algorithm for L2 optimal transport in 3D, Lévy, Mathematical Modeling and Analysis, 2015, arXiv:1409.1279 [math.AP]; Video: Semi-discrete Optimal Transport and some of its application, summer school on geometric measure theory.

Miguel Couceiro et Chedy Raïssi: Recherche de motifs et théorie de l'agrégation en analyse de données.

Propositions de stages

Voici des propositions de stage ; n'hésitez pas à contacter les orateurs de la journée pour d'autres propositions.

• Jean-Baptiste Mouret :
  1. Reactive controllers for hexapod robot
  2. Recovering from a sequence of damages with fast trial-and-error learning
  3. Probabilistic Motion Primitives Without Demonstrations
  4. Learning to crawl with a damaged iCub robot
• VeriDis :
  1. Proving preprocessing for Satisfiability Modulo Theories
  2. Generating Counterexamples for Coq and TLA+ Proof System
• Olivier Devillers :
  1. Longueur de chemins et de leur discrétisation
  2. Itérer sur les plus proches voisins d'un point
  3. Stretch facteur du chemin des plus proche voisins
• Bruno Lévy
  1. A geometric algorithm for implementing Yann Brenier's "transport-collapse" scheme in 3D
  2. Certified code generation for geometric predicates
• Slim Ouni
  1. Modélisation dynamique d'une langue 3D en utilisant un articulographe
  2. Modeling facial expressions for a virtual 3D talking head
  3. PuppetFace: Contrôle et animation d'une tête parlante 3D en temps réel
• Jérémie Dumas
  1. Anisometric texture synthesis optimization
  2. Discrete Voronoi Diagrams and Applications to Surface Offsetting
• Jannik Dreier et Steve Kremer
  1. Equational Theories in the Tamarin Security Protocol Verifier
• Michaël Rusinowitch
  1. Privacy Control for Online Social Networks

---

Contacter le Département Informatique
Dernières modifications : le 20/12/2015