|
SL306-1 Modelisation par éléments finis d'un actionneur micro fluidique
|
|
|
Description
|
|
Les technologies de base micro/nanofluidiques atteignent une maturité suffisante pour entrevoir de fortes potentialités pour des applications qui s'étendent des sciences du vivant (criblage de médicament, séquençage ADN et diagnostics) jusqu'à la santé (systèmes embarqués d'injection ou de prélèvement) en passant par la chimie. Pour injecter, prélever ou transférer un fluide dans une micro canalisation, il est important de disposer de micro et même nano actionneurs embarqués. Les niveaux d'intégration (100µm²-10000µm²) et les densités (>1000) que mettent en jeu les micro plates-formes fluidiques pour le diagnostic sont nouvelles dans le domaine du microactionnement. Pour ces niveaux d'intégration (>1000 act/cm2), les actionneurs doivent être totalement intégrables (évite les connections qui constituent un point dur), précis, simples, extrêmement compacts (µm²) tout en restant relativement puissants (>kPa,>10µm de déflexion) et bien sûr bio compatibles.
Nous développons des micro/nano actionneurs pyrotechniques très compacts intégrés dans la canalisation. Ces actionneurs comportent une membrane élastique de PDMS qui sous l'effet d'une surpression générée par un matériau énergétique vient obturer la canalisation fluidique ou pousser un fluide présent dans la canalisation.
Ce projet fait l'objet d'une thèse et d'un financement ANR de 3 ans. L'étudiant en stage s'intègrera donc dans l'équipe et travaillera en étroite collaboration avec le thésard.
Le travail de stage proposé concerne la mise en équation et la modélisation multiphysique par éléments finis du fonctionnement du micro actionneur. En effet, bien comprendre la physique (thermodynamique et fluidique) sur la base de laquelle ces actionneurs fonctionnent est d'autant plus importante que l'actionnement doit être fin et contrôlé en pression et température.
La modélisation sera supportée par laplate-forme logicielle COMSOL Multiphysique
URL sujet détaillé :
:
Remarques : oui
|
|
|
|
|
|
SL306-2 Etude algorithmique de graphes arête-coloriés
|
|
|
Description
|
|
Le sujet porte sur l'exploration algorithmique de graphes dont les arêtes sont coloriées par k couleurs, pour k donné. Une telle étude est motivée par les applications importantes de ces graphes en VLSI et surtout en biologie (structures ADN). A partir d'un graphe dont les arêtes sont coloriées par k couleurs, nous cherchons à extraire de sous-structures avec de propriétés spécifiques sur la coloration des arêtes. Par exemple, cycles et chaînes hamiltoniens alternés (deux arêtes adjacentes du cycle ayant de couleurs differentes), parcours euleriens alternés, arbres couvrants proprement coloriés etc.
Travail demandé : Pendant une premièr temps, effectuer une étude bibliographique et exploration du terrain. Dans un deuxième temps, effectuer de la recherche en plein sens du terme en essayant de résoudre quelques problèmes relatifs au sujet.
Références
1. A. Benkouar, Y. Manoussakis, V. Paschos, R.Saad On the complexity of Hamiltonian and Eulerian problems in edge-colored complete graphs, RAIRO Journal On Operations Research Vol. 30 No 4 (1996) 417-438.
2. J. Bang-Jensen, G Gutin A.Yeo, Properly coloured hamiltonian paths in edge-colored complete graphs, Discrete Applied Mathematics 83 (1998) 267-270.
URL sujet détaillé :
:
Remarques : Pas de possibilité de rénumération. Le sujet peut conduire à une thèse, plus tard.
|
|
|
|
|
|
Fanny DUFOSSE : SL306-3 Etude algorithmique des jeux basés sur des modèles de graphes
|
|
|
Description
|
|
La théorie algorithmique des jeux est une émanation de la théorie des probabilités et de l'algorithmique. Elle représente l'application des mathématiques à la description et à la résolution algorithmique des problèmes liés aux jeux selon un modèle mathématique donné (matrice, graphe etc.). C'est John Von Neumann qui est le père de la théorie des jeux, en démontrant en 1928 le théorème le plus important dans ce domaine (le théorème du minimax), et en écrivant en 1944 avec O.Morgenstern l'ouvrage référence sur le sujet La théorie des jeux et le comportement économique.
Les principales approches traditionnelles dans le domaine, concernent des systèmes centralisés dans lesquels les agents coopèrent afin de atteindre un but commun. Avec l'arrivée d'Internet, il est apparu nécessaire d'étudier un nouveau comportement d'agents avec des interactions contradictoires. Par exemple, un utilisateur normal d'Internet et un expéditeur de spam's sont deux agents avec des objectifs opposés : le 1er souhaite minimiser le nombre de spams qu'il reçoit, tandis que le 2eme souhaite maximiser le nombre de spams à envoyer. Les concepts utilisés pour modéliser de tels systèmes sans contrôle centralisé, sont ceux de l'équilibre de Nash et la mesure du rapport de coordination (ou prix de l'anarchie) [5]. Parmi tous les états possibles d'un jeu donné, l'équilibre de Nash est définie comme un état dans lequel aucun agent n'a intérêt à changer sa stratégie. Il est à noter que plusieurs états peuvent amener à une équilibre de Nash et par conséquent la solution obtenue n'est pas toujours unique et peut conduire à des performances plus ou moins bonnes. Le rapport de coordination est une mesure de qualité de l'équilibre de Nash obtenue.
Dans le cadre de cette étude, nous considérons un problème de sécurité sur un réseau modélisé par un graphe G [1]. Sur un tel jeu il y a deux types de joueurs, les attaquants (virus etc.) et les protecteurs (logiciels de protection etc.) . L'attaquant utilise une distribution de probabilité afin de choisir les nóuds du réseau à endommager. A l'opposé, le protecteur, en utilisant une autre distribution de probabilité, choisit une partie du réseau (i a sous graphe H de G) à nettoyer. Dans un tel scénario, l'objectif de l'attaquant est de maximiser la probabilité d'échapper à un nettoyage possible tandis que l'objectif du protecteur est de maximiser le nombre de nóuds à nettoyer.
Ce type de jeu non coopératif a été étudié dans le cas où la partie du réseau considéré par le protecteur est une arrête ou un chemin ou un ensemble d'arrêtes [1-4], i.e., lorsque le sous graphe H de G est isomorphe à une arrête ou un chemin, ou un ensemble d'arrêtes dans G. Ici nous proposons de généraliser les résultats obtenus dans [1-4], en considérant n'importe quel sous graphe H des familles de graphes G (graphes parfaits, planaires bipartis etc.).
Références
1. M. Mavronicolas, V. Papadopoulou, A. Philippou and P. Spirakis, "A Graph-Theoretic Network Security Game", Proceedings of the First Workshop on Internet and Network Economics (WINE 2005), LNS Springer-Verlag, Hong Kong, December 2005, to appear.
2. M. Mavronicolas, P. Panagopoulou, and P. Spirakis, "Cost Sharing Mechanisms for Fair Pricing of Network Usage", Proceedings of the Dagstuhl Seminar on Algorithmic Aspects of Large and Complex Networks (Dagstuhl Seminar Series 05361), September 2005, to appear
3. M. Mavronicolas, V. Papadopoulou, A. Philippou and P. Spirakis, "A Network Game with Attacker and Protector Entities", Proceedings of the 16th Annual International Symposium on Algorithms and Computation (ISAAC 2005), Lecture Notes in Computer Science Springer-Verlag, Sanya, Hainan, China, December 2005, to appear.
4. R. Elsδsser, M. Gairing, T. Lόcking M. Mavronicolas and B. Monien "A Simple Graph-Theoretic Model for Selfish Restricted Scheduling", Proceedings of the First Workshop on Internet and Network Economics (WINE 2005), LNCS, Springer-Verlag, Hong Kong, December 2005, to appear
5. MJ. Osborne and A. Rubinstein, A course in Game Theory, MIT Press, 1994.
URL sujet détaillé :
:
Remarques : Pas de possibilité de rénumération. Le sujet peut conduire à une thèse, plus tard.
|
|
|
|
|
|
SL306-4 Clôture par intersection des congruences
|
|
|
Description
|
|
Présentation générale du sujet :
Étant donnée une relation d'équivalence, sa clôture de congruence, par rapport à un ensemble fini d'opérations F est la plus petite relation d'équivalence compatible avec F. De nombreux algorithmes ont été proposés pour le calcul de la clôture de congruence, qui joue un rôle central dans la combinaison de techniques de décision et l'analyse de programmes. Le sujet porte sur les opérations possibles sur les clôtures de congruence et notamment sur leur stabilité par intersection.
Objectif du stage :
On considère le problème suivant: étant donnés deux ensembles finis d'équations (entre termes) E1 et E2, chacun d'eux engendre une clôture de congruence (=E1 et =E2 respectivement). L'intersection =E1 ∩ =E2 peut-elle être exprimée comme la clôture de congruence d'un ensemble fini d'équations =E ? Autrement dit:
Quand l'intersection de deux congruences
finiment engendrées est elle finiment
engendrée ?
On montrera d'abord que c'est toujours le cas lorsque les symboles de l'alphabet sont unaires (i.e. sur les mots) et faux en général pour les termes. Puis le problème est de donner des conditions suffisantes aussi générales que possibles.
Il pourra être utile d'utiliser des techniques d'automates, notamment d'automates sur les relations.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Nicolas PERRIN : SL306-5 Automates avec visibilité et automates à mémoire
|
|
|
Description
|
|
Présentation générale du sujet :
Dans [1], les auteurs ont introduit une classe de langages (visibly pushdown) qui, bien que strictement plus générale que les langages réguliers, en possède toutes les bonnes propriétés.
Dans [2], les auteurs ont introduit une classe de langages d'arbres (à une mémoire) qui généralise les automates à piles de mots et possède des bonnes propriétés de décision, mais pas de bonnes propriétés de clôture.
Le sujet porte sur la combinaison de ces deux résultats.
Objectif du stage :
L'objectif est de définir une classe d'automates à une mémoire, s'inspirant des visibly pushdown et qui permette de rétablir les propriétés de clôture perdues dans [2].
Comme extensions possibles: une telle classe de langages pourrait être utilisée pour résoudre des contraintes ensemblistes de manière efficace et donc en analyse de programme.
Pré-requis : Connaissances de base sur les automates finis et les automates à pile
Bibliographie :
[1] R. Alur and P. Madhusudan. Visibly pushdown languages Proc. STOC. 2004.
[2] H. Comon-Lundh and V. Cortier. Tree automata with one memory, set constraints and cryptographic protocols. TCS 331, 2005.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL306-6 Implantation des fonctions élémentaires avec arrondi correct
|
|
|
Description
|
|
Le calcul en virgule flottante est normalisé depuis 1985: la norme
définit non seulement les formats (simple et double précision) avec
leurs cas exceptionnels (infinis, erreurs, ...), mais aussi le
comportement des quatre opérations et de la racine carrée. Par
exemple, lorsque vous faites une addition flottante, il arrive que le
résultat soit arrondi, mais la norme exige que le résultat retourné
soit le nombre flottant le plus proche du résultat mathématique
exact. Cette propriété s'appelle l'arrondi correct. Ceci permet en
principe d'écrire du code numérique portable d'un système à l'autre,
et aussi d'écrire des théorèmes sur le comportement numérique d'un
code qui seront valables d'un système à l'autre.
Malheureusement, ces bonnes propriétés s'évaporent dès qu'un morceau de code
contient une fonction élémentaire (sin/cos, exp/log, ...) : les fonctions
élémentaires ont été laissée en dehors de la norme sur la virgule flottante.
Une raison en est qu'en 1985 on ne savait pas garantir l'arrondi correct
d'une fonction transcendante. Aujourd'hui on sait, et le projet Arénaire
développe actuellement une bibliothèque mathématique (crlibm) offrant
l'arrondi correct pour les fonctions élémentaires. L'objet de ce stage est
d'implémenter des fonctions manquant actuellement à cette bibliothèque:
trigonometriques et hyperboliques inverses, fonction puissance, fonctions
spéciales.
L'étudiant devra, pour chaque fonction traitée, définir un algorithme
adapté en s'inspirant de la littérature, et l'implémenter en C
portable, avec un souci de correction et de performance. L'algorithme
retenu devra utiliser uniquement les briques de bases offertes par les
processeurs pour le calcul entier et flottant : essentiellement les
quatre opérations. Typiquement, une fonction élémentaire est donc
approchée par un polynôme sur un petit intervalle, et une étape
préliminaire de réduction d'argument ramène tout nombre en entrée dans
cet intervalle.
La difficulté est qu'on doit, pour garantir l'arrondi correct, majorer
très finement les différentes erreurs qui interviennent dans ce
processus : erreur d'approximation de la fonction par un polynôme dont
les coefficients sont contraints à être des flottants, erreurs
d'arrondi qui s'accumulent au long du calcul, etc. Des exemples de ce
travail sont donnés en [5]. L'étudiant devra faire preuve d'intuition
mathématique aussi bien qu'informatique pour gérer les nombreux
compromis entre précision et performance qui interviennent à tous les
niveaux.
Les techniques pour l'arrondi correct sont désormais bien
maîtrisées, et la recherche est actuellement dans deux directions:
- les techniques de calcul d'erreur, avec un recours croissant a des
outils de preuve formelle [3],
- les optimisations fines dépendant de l'architecture [4].
L'intérêt de ce stage est donc d'aller des mathématiques (analyse)
vers une implémentation de bas niveau, en passant par l'utilisation
d'assistants a la preuve formelle.
Bibliographie:
[1] J._M. Muller. Elementary Functions, Algorithms and
Implementation. Birkhauser, 1997.
[2] P. Markstein. IA-64 and Elementary Functions : Speed and
Precision, Prentice Hall, 2000
[3] F. de Dinechin, C. Lauter, G. Melquiond. Assisted verification of
elementary functions.
http://www.ens-lyon.fr/LIP/Pub/Rapports/RR/RR2005/RR2005-43.pdf
[4] F. de Dinechin, A. Ershov, N. Gast. Towards the post-ultimate libm.
IEEE Arith 17.
http://perso.ens-lyon.fr/florent.de.dinechin/recherche/publis/2005-Arith.pdf
[5] The crlibm project:
http://lipforge.ens-lyon.fr/projects/crlibm/
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Etienne MIRET : SL306-7 Outils de maintenance pour les preuves formelles
|
|
|
Description
|
|
Il s'agit de concevoir et de développer un environnement de travail, éventuellement multi-processus pour faciliter la ré-ingéniérie des
documents formels intervenant dans une preuve.
En première analyse, on se concentrera sur les démonstrations effectuées à l'aide du système Coq, mais une extension séduisante de se travail devrait permettre la transformation semi-automatique de preuves formelles obtenues avec un système de démonstration en des preuves utilisées avec un autre système de démonstration.
URL sujet détaillé : http://www-sop.inria.fr/marelle/Yves.Bertot/stage-rip.html
Remarques : L'étudiant sera rémunéré s'il ne dispose pas
déjà d'un financement.
|
|
|
|
|
|
SL306-8 Etude des rotations non isomorphiques pour la manipulation d'objets 3D dans une salle immersive.
|
|
|
Description
|
|
Titre: Etude des rotations non isomorphiques pour la manipulation d'objets 3D dans une salle immersive.
Contexte du sujet:
------------------
Supposons que nous disposions d'une boule de pétanque (Sud de la France oblige ...) dont nous pouvons constamment déterminer son orientation dans l'espace. Cette boule de pétanque peut permettre de faire tourner un objet virtuel dans une scène 3D (et même une boule de pétanque virtuelle) ou faire faire tourner le point de vue de l'utilisateur. Une façon très simple de relier les orientations de la boule de pétanque réelle et les orientations dans la scène virtuelle est
de les faire correspondre directement. Ainsi, une rotation de 15 degrés dans le plan horizontal de la boule de pétanque réelle conduit à
une rotation de 15 degrés dans le même plan de l'objet virtuel. Dans certaines conditions que l'on explicitera, la souplesse de nos poignets, par exemple, peut contraindre les mouvements 3D. Ainsi, on peut être amené à effectuer des rotations dites "non isomorphiques" car ne correspondant pas exactement aux rotations initiales mais à une transformation de ces rotations soit amplifiée, soit atténuée. Une
autre façon de soulager les poignets, pour reprendre cet exemple, consiste à permettre de reposer la boule de pétanque et à la reprendre
dans une autre position, à la façon de la souris.
On s'intéresse à comparer ces modes de rotations.
Ce qui existe:
--------------
Une centrale inertielle 3D est insérée dans une boule de pétanque permettant ainsi de connaître constamment les trois angles d'Euler. Une application minimale permet de faire tourner un cube selon ces trois angles. La mise à zéro de la position n'est pas gérée actuellement.
Le travail à effectuer:
-----------------------
- Étudier ce qui est déjà fait dans la littérature (Foley, LaViola, ...): faire un inventaire des transformations sur les rotations et les classer selon des critères à déterminer.
- Implémenter ces différents modes de rotations. Apparemment triviale, l'implémentation nécessite de bien appréhender les rotations dans l'espace. La représentation en angles d'Euler (fournie par la centrale inertielle) est loin d'être la plus adaptée. On s'intéressera plutôt à des représentations en quaternions. Des transformations non linéaires peuvent conduire à des situations pas forcément intuitives de la part de l'utilisateur: il se peut alors qu'en revenant à la position physique initiale de la boule, la boule virtuelle ne soit plus à sa position initiale !
- Tester et classer éventuellement en fonction des tâches à effectuer. Etablir la liste des avantages et inconvénients.
- Chercher (et trouver ?) des nouvelles transformations permettant de conserver les avantages et de minimiser les inconvénients des transformations existantes.
Environnement de travail:
-------------------------
Le stage s'effectuera dans les locaux de l'École Polytechnique Universitaire de Nice - Sophia Antipolis, au département Informatique où
est hébergée l'équipe Rainbow de l'I3S (UMR 6070 Univ. Nice - Sophia Antipolis, CNRS).
Le stagiaire disposera d'un PC récent avec carte graphique 3D sous Linux ainsi que d'une centrale inertielle 3D (InterSense InertiaCube3) insérée
dans une boule de pétanque. Différents autres périphériques 3D sont disponibles dans l'équipe si besoin est. Il aura accès à une salle immersive afin d'effectuer les tests nécessaires au sujet.
Des connaissances en C++, Qt et OpenGL seront un plus.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Jerome CONTANT : SL306-9 Chemins hamiltoniens dans un graphe triangulé
|
|
|
Description
|
|
La démonstration du théorème des quatre couleurs commence par une réduction du problème à celui de l'existence d'un chemin 'hamiltonien' (en un sens à préciser) dans une triangulation d'un graphe planaire.
Le sujet du stage est dans un premier temps, théorique, de maîtriser les fondements mathématiques de cette réduction, puis dans un second temps de réaliser un programme graphique permettant l'affichage d'un graphe triangulé et la recherche interactive d'un chemin 'hamiltonien'.
URL sujet détaillé :
:
Remarques : Le stage devra se terminer au plus tard fin juillet.
Pas de financement prévu côté IML.
|
|
|
|
|
|
SL306-10 Estimation de coûts d'exécution pour l'ordonnancement de calculs sur grille
|
|
|
Description
|
|
Le projet RAINBOW du laboratoire CNRS I3S s'intéresse à la mise en oeuvre d'applications réparties sur des grilles de calcul et de données. Une grille offre un
support pour la réalisation de calculs coûteux et le stockage de données massives dont peuvent bénéficier nombre d'applications, notamment des applications au traitement d'images médicales faisant intervenir de grandes bases de données à analyser. Ce type d'application nécessite en outre l'assemblage de nombreux algorithmes de traitement, plus ou moins coûteux, dans un flot applicatif complexe. Nous avons développé un moteur de gestion de flot parallélisé, MOTEUR, pour répondre à ce besoin. Notre recherche porte sur l'optimisation du temps de calcul par une bonne prise en
compte des ressources disponibles sur la grille en fonction des besoins de calcul. Elle s'appuie sur des travaux antérieurs d'optimisation de tâches sur des architectures parallèle mais nécessite la réexpression des problèmes sur une nouvelle infrastructure de grille dont les paramètres diffèrent sensiblement d'infrastructures antérieures (latence très important, taille sans précédent, volatilité de l'infrastructure...).
Le sujet de ce stage porte sur l'estimation des temps d'exécution des processus impliqués dans le flot applicatif pour permettre une meilleur répartition des tâches de calcul sur les ressources disponibles. Le travail consistera à proposer une modélisation du temps d'exécution des codes applicatifs en fonction du volume de données à traiter. Le modèle sera mis en oeuvre et testé sur une infrastructure de grille de production. La mise en oeuvre devra permettre une mise à jour dynamique des paramètres du modèle pour permettre l'adapatation des estimations en fonction des évolutions de l'infrastructure.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Bertrand MARC : SL306-11 Calcul de polyèdres dans la vérification de systèmes hybrides
|
|
|
Description
|
|
Récemment les systèmes hybrides (c'est-à-dire des systèmes avec des dynamiques continues et discrètes) ont reçu beaucoup d'attention de la communauté scientifique. Des techniques d'analyse de ces systèmes ont de nombreuses applications, telles que la validation de systèmes embarqués (avionique, automobile, puissance) et des circuits analogiques ainsi que l'étude de modèles bio-chimiques.
L'étape de base dans la vérification de systèmes continues et hybrides est le calcul (souvent approximatif) de l'ensemble d'états atteignables d'un système défini par des équations différentielles. Le calcul est souvent basé sur une combinaison des techniques de l'intégration numérique, de la géométrie algorithmique et de l'optimisation. Nous allons concentrer notre attention sur une approche qui représente des ensembles d'états atteignables (qui sont des sous-ensembles de R^n) par des polyèdres.
L'objectif de ce projet est d'étudier la possibilités d'utiliser des bibliothèques standard dans l'implantation des algorithmes de vérification de systèmes hybrides. Une question théorique importante est d'analyser et de quantifier l'influence des imprécisions dans des opérations polyèdriques sur la robustesse des algorithmes de vérification.
Cette étude s'effectuera à travers l'analyse des exemples de l'outil de vérification d/dt (développé à Verimag) et de la bibliothèque de polyèdres Parma (développée à l'université de Parma). Les résultats seront appliqués sur des modèles hybrides des circuits analogiques et mixtes
Le candidat devrait avoir des compétences suivantes :
1) Connaissance de base de l'algèbre linéaire et de la géométrie algorithmique
2) Capacité d'apprendre et d'utiliser de nouveaux logiciels
Le stage va s'effectuer au laboratoire Verimag à Grenoble, un des centres de recherche principaux dans le domaine des systèmes embarqués et hybrides.
URL sujet détaillé : http://www-verimag.imag.fr/~tdang/stage-poly.html
Remarques : Posibilité de rénumération : oui
|
|
|
|
|
|
SL306-12 Ordonnancement régulé pour systèmes embarqués fiable
|
|
|
Description
|
|
À partir d'un DAG de tâches avec contraintes de précédence et d'une
architecture répartie hétérogène, il s'agit de produire un
ordonnancement multi-processeurs des tâches sur l'architecture, en
minimisant le makespan, maximisant la fiabilité, et en maximisant le
niveau de qualité des tâches. L'originalité du problème réside dans
l'utilisation des résultats récents sur l'ordonnancement régulé. Cette
technique d'automatique des systèmes continus permet de contrôler
en-ligne les paramètres d'un ordonnancement en fonction de grandeurs
mesurées en temps-réel sur celui-ci. Dans notre cas, c'est la
fiabilité qui servira de mesure pour la régulation.
URL sujet détaillé : http://pop-art.inrialpes.fr/~girault/Projets/Scheduling/ordo-regule-fiabilite-ens-2006.pdf
Remarques :
|
|
|
|
|
|
SL306-13 Extraction de la structure modulaire des graphes pour la comparaison des réseaux biologiques
|
|
|
Description
|
|
Contexte :
--------
Les gènes et leurs produits, les protéines, ne peuvent rendre compte du fonctionnement global d'un organisme vivant quand on les étudie chacun séparément : bien que l'attribution de fonctions biologiques se fasse surtout au niveau des gènes individuellement, la structure des interactions entre les gènes permet de repérer des groupes fonctionnels et ainsi d'attribuer des fonctions à des groupes de gènes. Ces interactions peuvent être modélisées par des graphes dont les sommets représentent les gènes d'un organisme vivant et les arêtes des interactions entre ces gènes.
Le développement des méthodes expérimentales en biologie permet aujourd'hui d'avoir un nombre restreint mais croissant de graphes représentant les interactions entre les gènes à l'échelle d'un organisme vivant. Les graphes considérés ont ainsi plusieurs milliers de sommets (un être humain a entre 20000 et 25000 gènes).
Objectif :
--------
Il s'agit de repérer des groupes fonctionnels en comparant les graphes d'interaction disponibles pour plusieurs espèces. Cette comparaison passe par une mise en correspondance des sommets des graphes et on dispose pour cela d'une relation entre les sommets des graphes (représentant la similarité entre couple de gènes par exemple). Ainsi, étant donnés plusieurs graphes d'interaction et une relation de correspondance entre les sommets de ces graphes, on cherche les sous-ensembles de sommets qui partagent une propriété donnée (par exemple, de connexité ou de densité) dans la plupart des graphes.
Le sujet de ce stage consiste à développer une méthode générique pour trouver ces groupes fonctionnels, en s'inspirant de plusieurs techniques développées pour des cas particuliers. Ce travail nécessitera une recherche en algorithmique, un développement et des tests sur les données biologiques.
Aucune connaissance en biologie n'est requise pour commencer ce sujet, cependant un intérêt pour l'application et une motivation pour le travail pluridisciplinaire sont préférables.
URL sujet détaillé :
:
Remarques : Co-encadrement avec Frédéric Boyer du Laboratoire de Biométrie et Biologie évolutive, UMR 5558
|
|
|
|
|
|
SL306-14 Analyse et documentation du protocole de synchronisation iSync
|
|
|
Description
|
|
Le système d'exploitation MacOS X comporte un moteur de synchronisation
iSync. iSync permet à un utilisateur de conserver plusieurs copies de
divers types de données complexes, par exemple ses calendriers, son
carnet d'adresse, ses mots de passe, ses signets Web, etc.
L'utilisateur peut mettre à jour n'importe quel réplicat de façon
déconnectée ; iSync fusionnera les différentes mises à jour, tout en
détectant les conflits éventuels, qui seront proposés à l'utilisateur
pour résolution manuelle. iSync se différencie donc des autres
logiciels similaires car c'est un moteur de réconciliation général, qui
s'adapte à la sémantique des données répliquées. Les API et
l'utilisation d'iSync sont bien documentés, mais son fonctionnement
interne est mal connu. Le stagiaire étudiera et documentera ce
fonctionnement, par analyse de la documentation existante, par la mise
en oeuvre expérimentale d'un nouveau type de données partagées, et par
l'observation externe grâce à l'outil d'analyse de protocoles Pandora.
URL sujet détaillé :
:
Remarques : Le stage se déroule au sein du projet commun INRIA-LIP6 Regal
, qui étudie les systèmes répartis à grande
échelle de type P2P. Un axe important est la réplication et le maintien
de la cohérence tenant compte de la sémantique des données. Le lieu de
travail est le LIP6 à Paris XVème arrondissement.
Possibilité de rénumération.
|
|
|
|
|
|
SL306-15 Model-checking symbolique et accélération de systèmes à compteurs
|
|
|
Description
|
|
FAST est un outil de vérification automatique des systèmes à
compteurs qui met en oeuvre une approche innovante combinant
arithmétique de Presburger et accélération de
circuits. Les algorithmes incarnés dans
FAST permettent souvent de calculer de façon exacte l'ensemble des
états accessibles de systèmes complexes, où l'évolution de nombreux
compteurs dépend de conditions interdépendantes.
L'objectif du stage est d'améliorer les techniques utilisées dans
FAST en tirant au mieux partie des variables bornées (booléens,
contrôle) du système
à analyser. À l'heure actuelle ces variables sont
considérées comme des compteurs arbitraires. Nous espérons être
capables d'analyser des systèmes plus larges en prenant mieux en compte la
structure de contrôle.
Le travail demandé consiste à
assimiler les techniques de model-checking symbolique (notamment les BDD,
diagrammes de décision binaire) et
reformuler les algorithmes de FAST dans un cadre basé sur les
BDDs.
Si le temps le permet et/ou si le candidat le désire, on évaluera la
pertinence des algorithmes proposés
via une implémentation de type maquette (en C++). Il s'agit de mesurer sur desexemples canoniques les avantages de la nouvelle approche.
Prérequis : Bases en logique, en théorie des automates, et en algorithmique.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/l3-06-pssb-1.html
Remarques : Co-encadrant: Sebastien Bardin
|
|
|
|
|
|
SL306-16 Agencement de graphes et géolocalisation
|
|
|
Description
|
|
Le but du stage est d'arranger dans le plan un graphe quasi-arborescent dont certains sommets sont fixés. Plus concrètement, le graphe sera une vue partielle du réseau Internet, obtenue depuis une source, et les sommets fixés seront les routeurs dont on connait le couple (longitude, latitude), le but étant de situer le graphe observé sur une carte du monde.
Pour un exemple de graphe obtenu sans placement géographique, voir http://www.liafa.jussieu.fr/~fabien/store/radar_example.pdf
Le programme serait le suivant :
Semaine 1-2: Introduction au projet et aux outils, réunion avec des experts en géolocalisation et élaboration d'un outil capable de récupérer les couple longitude/latitude grâce aux outils Web existants.
Semaine 2-3-4-5: Réflexion sur l'algorithme de placement des noeuds non localisés, puis codage et essais avec nos outils de visualisation.
Semaine 6 (et + si motivé): Finition d'un code opérationnel et integrable dans le projet. Éventuellement, travail sur la visualisation avec carte du monde en arrière-plan
URL sujet détaillé : Voir éventuellement ébauche d'article : http
Remarques : Co-encadrement avec Fabien Viger : fabien.jussieu.fr
(Merci de l'inclure en Cc dans les réponses)
Possibilité de rémunération si élève non salarié.
|
|
|
|
|
|
SL306-17 Opérateurs morphologiques pour le contrôle de la topologie de modèles volumiques
|
|
|
Description
|
|
Contexte
Ce projet se situe dans le domaine de l'informatique graphique, et plus exactement de la manipulation d'objets 3D virtuels, obtenus par numérisation de modèles réels. Pour peu qu'un modèle soit complexe, cette numérisation (typiquement, par scanner) peut s'avérer imprécise et génèrer des petits artefacts topologiques sur les objets : parties connectées alors qu'elles ne devraient pas l'être (cf. figure), trous, ... Plusieurs méthodes ont été proposées pour "réparer" les objets, mais aucune ne permet de gérer de manière interactive leur topologie, c'est-à-dire leur nombre de composantes connexes et de trous, ainsi que l'emplacement de ceux-ci.
Nous travaillons en partenariat avec le département d'informatique de l'Université Polytechnique de Catalogne à Barcelone (Pere Brunet, Carlos And=FAjar, =C1lvar Vinacua, Jordi Esteve) sur une méthode qui résoudrait ce problème. La méthode se déroule en plusieurs étapes :
1. conversion de l'objet initial, une surface triangulée, en ensemble de voxels connectés par leurs faces et d'épaisseur 1, appelé membrane discrète ;
2. application d'opérateurs de morphologie mathématique (érosion, dilatation, ouverture, fermeture) sur cette membrane discrète ;
3. détection des zones où la topologie a été modifiée ;
4. affichage de ces zones dans une interface de visualisation et interaction avec l'utilisateur pour savoir si elles doivent être conservées ou non ;
5. conversion du modèle volumique résultant de ce choix en surface triangulée.
Objectifs
Le travail proposé pour ce projet concerne les étapes 2 à 4 de cette démarche. Après une mise à jour de ses connaissances mathématiques (topologie des surfaces et des volumes, morphologie), le stagiaire implémentera des méthodes efficaces de calcul des opérateurs morphologiques sur un ensemble de voxels, et évaluera l'influence de ceux-ci sur la modification de la topologie des objets. Il en tirera un bilan critique sur l'efficacité de la méthode proposée. Les données nécessaires aux tests, ainsi que l'interface de visualisation, seront fournies par l'encadrant.
Mots-clés : voxel, morphologie mathématique, topologie combinatoire, informatique graphique, traitement d'images.
URL sujet détaillé : http://www-evasion.imag.fr/Membres/Franck.Hetroy/Students/sujet_l3.html
Remarques :
|
|
|
|
|
|
Louis DROUNAU : SL306-18 Modelage interactif d'une argile virtuelle
|
|
|
Admin
|
|
| Encadrant : Marie-paule CANI |
| Labo/Organisme : il s'agira de reprendre le modèle d'argile virtuelle à trois couches (déformations globales, déformations locales, et tension de surface) mis au point par Guillaume Dewaele pendant sa thèse, et de l'interfacer avec une main déformable, servant d'outil, dont le modèle est fourni par Paul Kry. Le modèle d'argile est basé sur une représentation implicite des surfaces (densité de matière stockée dans une grille 3D), ce qui permet de courvir toute géométrie et de modéliser les changements de topologie. La main, basée sur un modèle Poser (Curious Labs / e frontier), offre des déformation réalistes de la chair en fonction de la position de son squelette articulé. |
| URL : http://www-evasion.imag.fr/Membres/Marie-Paule.Cani/ |
| Ville : Grenoble |
|
|
|
|
Description
|
|
La création d'images de synthèse repose sur la modélisation géométrique d'objets, de formes et genres topologiques variés. Les systèmes classiques de modélisation sont loin d'être intuitifs: l'utilisateur déplace par exemple les points de contrôle d'une surface paramétrique, ce qui l'oblige à connaitre la représentation mathématique sous-jacente, impose des interfaces complexes, et restreint la classe des surfaces modélisées.
L'objectif de ce stage est de participer à la mise au point d'un sytème de sculpture interactive qui s'inspire de la manipulation d'argile ou de pâte à modeler : il s'agira de reprendre le modèle d'argile virtuelle à trois couches (déformations globales, déformations locales, et tension de surface) mis au point par Guillaume Dewaele pendant sa thèse, et de l'interfacer avec une main déformable, servant d'outil, dont le modèle est fourni par Paul Kry. Le modèle d'argile est basé sur une représentation implicite des surfaces (densité de matière stockée dans une grille 3D), ce qui permet de courvir toute géométrie et de modéliser les changements de topologie. La main, basée sur un modèle Poser (Curious Labs / e frontier), offre des déformation réalistes de la chair en fonction de la position de son squelette articulé.
La réalisation de l'interface sera abordée de la manière suivante: La position et la posture de la main seront contrôlés interactivement par l'intermédiaire d'un bras à retour d'effort (dispositif "Phantom"), que l'on complètera par des capteurs de pression pour estimer l'intensité de prise de l'utilisateur.
La main virtuelle effectuera des mouvements de pincement, controlés par la pression de la main réelle sur le stylet. Outre les déformations de l'argile, un retour d'effort pourra être restitué, en s'inspirant des modèles proposés à EVASION par Renaud Blanch et Eric Ferley.
Bibliographie:
-----------------
Interactive global and Local Deformations for Virtual Clay
Guillaume Dewaele, Marie-Paule Cani
Graphical Models (GMOD), Volume 66, page 352-369 -
sep 2004
http://www-evasion.imag.fr/Publications/2004/DC04a/
Virtual Clay for Direct Hand Manipulation
Guillaume Dewaele, Marie-Paule Cani
Eurographics (short papers) - 2004
http://www-evasion.imag.fr/Publications/2004/DC04/
Non-Realistic Haptic Feedback for Virtual Sculpture
Renaud Blanch, Eric Ferley, Marie-Paule Cani, Jean-Dominique Gascuel
Technical Report RR-5090, INRIA, Number RR-5090 -
January 2004
http://www-evasion.imag.fr/Publications/2004/BFCG04/
URL sujet détaillé :
:
Remarques : Co-encadrants:
- Guillaume Dewaele (ATER en physique à ENS Lyon)
- Paul Kry (postdoc dans l'équipe EVASION du labo GRAVIR)
|
|
|
|
|
|
Anne-Cecile ORGERIE : SL306-19 Protocoles de transport hautes performances
|
|
|
Description
|
|
XCP (eXplicit Control Protocol) est un protocole de transport proposé par Dina Katabi (ACM SIGCOMM 2002). XCP représente une approche différente dans le domaine des algorithmes de contrôle de congestion, car il utilise l'assistance des routeurs. Cette approche est fondamentale pour les réseaux à grand produit bande passante X délai, où TCP est loin d'obtenir de bons résultats. XCP permet ainsi d'obtenir de hautes performances dans une large gamme d'infrastructure de réseaux.
Le protocole XCP est étudié depuis 2004 dans l'équipe RESO du LIP. Une approche originale de XCP est actuellement en cours de modélisation et de simulation dans l'équipe RESO (http://perso.ens-lyon.fr/dino-martin.lopez-pacheco/these/XCP/xcp-varenv.html).
Ce stage portera sur la mise en oeuvre et le déploiement de ce protocole de transport hautes performances fondé sur XCP. Le développement aura lieu dans le système d'exploitation Linux et pourra se baser sur des développements pré-existants. La validation de l'impleméntation aura lieu sur une plate-forme locale de test. Des expérimentations seront menées sur la plate-forme Grid5000 et devront démontrer les capacités d'extensibilité du protocole.
Competences requises : Programmation en C/JAVA - Connaissances sur le développement dans le noyau linux appréciées.
URL sujet détaillé : http://perso.ens-lyon.fr/laurent.lefevre/sujet_stage_L3.txt
Remarques :
Co-encadrement : Dino Lopez Pacheco (Equipe RESO / LIP) : http://perso.ens-lyon.fr/dino-martin.lopez-pacheco/
|
|
|
|
|
|
SL306-20 Maillage anisotrope par decimation
|
|
|
Description
|
|
Un maillage d'un domaine du plan ou de l'espace est une decomposition de ce domaine en triangles ou en tetraedres jointifs. Les maillages sont les ingredients de base des methodes de resolution d'equations aux derivees partielles par elements finis, qui permettent de simuler numeriquement l'ecoulement d'un fluide en presence d'un obstacle ou encore la deformation d'une piece mecanique sous contrainte.
Construire des maillages de qualite est un probleme algorithmique difficile et mal resolu dans le cas general. Les criteres de qualite dependent d'ailleurs du phenomeme qu'on desire simuler. Ainsi, en l'absence d'information a priori, on cherche le plus souvent a construire des maillages les plus isotropes possible, c'est-a-dire des maillages dont les elements (triangles ou tetraedres) sont le plus reguliers (equilateraux) possibles.
Pour des problemes de simulation specifiques, les maillages les plus ``efficaces'' sont anisotropes, c'est-a-dire que leurs elements doivent etre allonges dans certaines directions prescrites qui peuvent varier dans le domaine.
Recemment, on a propose une technique de maillage isotrope donnant des resultats largement superieurs aux methodes connues en dimension 3. Cette methode repose sur la minimisation d'une certaine energie associee au maillage et qui tend a favoriser les elements reguliers. Le but de ce stage est d'etendre cette methode au cas des maillages anisotropes, qui sont les plus utilises en calcul numerique. Le principe propose est de proceder par decimation : partant d'un maillage regulier fin de type grille, on va iterativement le simplifier en fusionnant des sommets de facon a minimiser une version anisotrope de l'energie utilisee dans le cas isotrope. Le stage consistera a essayer de faire marcher cette idee, d'abord dans des cas simples : en dimension 2, sans se preoccuper des problemes induits par le bord du domaine. Puis, si le temps le permet, on pourra tenter de traiter des cas plus generaux et plus realistes.
URL sujet détaillé : http://www-sop.inria.fr/geometrica/positions/index.html
Remarques :
|
|
|
|
|
|
SL306-21 Optimisation de l'arithmétique d'intervalles dans le compilateur GCC
|
|
|
Description
|
|
Dans le cadre de la standardisation ISO du language C++, nous proposons l'ajout d'une bibliotheque d'arithmetique d'intervalles. Nous aimerions apporter la preuve qu'il est facilement possible a un compilateur d'optimiser les changements de modes d'arrondis de la FPU automatiquement, ce qui permet de specifier une classe d'intervalles de maniere beaucoup plus simple tout en garantissant des bonnes performances.
Nous proposons donc de rajouter au compilateur GCC la reconnaissance des fonctions qui changent les modes d'arrondis, et le rajout d'optimisations qui permettent de les supprimer.
URL sujet détaillé : http://www-sop.inria.fr/geometrica/positions/sujet_compilateur.pdf
Remarques :
|
|
|
|
|
|
SL306-22 Test d'homotopie entre deux courbes tracées sur une surface
|
|
|
Description
|
|
Le stage proposé s'insère dans le domaine de la topologie algorithmique. Cette discipline a pour objet l'étude algorithmique de la topologie des objets combinatoires et connaît un regain d'intérêt comme en témoignent les récents tours d'horizon [1] et [2]. Un des aspects de cette discipline concerne la topologie des surfaces et plus particulièrement les courbes tracées sur les surfaces. Les ouvrages de Gross et Tucker [3] et Mohar et Thomassen [4] sont des références en la matière.
Une question fondamentale dans ce cadre est la suivante : Étant données deux courbes fermées C1 et C2 tracées sur une surface, peut-on déformer C1 en C2 de manière continue ? Dit autrement ces courbes sont elles homotopes ? Tamal Dey et Sumanta Guha ont proposé en 1999 [5] un algorithme de complexité linéaire (relativement à la taille des descriptions de la surface et des courbes) pour répondre à cette question. Leur algorithme repose sur la solution du problème de conjugaison tiré de la combinatoire des groupes [6] dans les cas particuliers étudiés. Le cas des surfaces orientables de genre 2 ou non-orientables de genre 3 ou 4 n'est cependant pas traité.
TRAVAIL DEMANDÉ :
L'objectif de ce stage est d'étudier et d'implémenter l'algorithme de Dey et Guha [5]. Si le temps le permet, une étude des cas non traités pourra être envisagées.
[1] T. K. Dey, H. Edelsbrunner, and S.Guha. Computational topology. In B. Chazelle, J.E. Goodman, and R. Pollack, editors, Advances in Discrete and Computational Geometry. AMS, 1998.
[2] G. Vegter. Computational topology. In J. E. Goodman and J. O'Rourke, editors, Handbook of Discrete and Computational Geometry, CRC Press. 1997.
[3] J. L. Gross and T. W. Tucker. Topological graph theory. Dover, 1987 (reprint 2001).
[4] B. Mohar and C. Thomassen. Graphs on Surfaces. John Hopkins University Press, 2001.
[5] T. K. Dey and Sumanta Guha. Transforming curves on surfaces. Journal of Computer and System Sciences, 58(2):297--325, 1999.
[6] R. Lyndon and P. Shupp. Combinatorial Group Theory. Springer-Verlag, 1977, volume 89, A Series of Modern Surveys in Mathematics.
URL sujet détaillé : http://www.lis.inpg.fr/pages_perso/lazarus/sujetsStage.html
Remarques :
|
|
|
|
|
|
SL306-23 Modélisation et analyse modulaires de réseaux géniques
|
|
|
Description
|
|
Les protéines assurent un grand nombre de fonctions dans les cellules.
Le taux de production de chaque protéine dépend de l'"état" de la
cellule et notamment, des concentrations des différentes protéines
présentes. Un tel réseau génique possède de nombreuses boucles de
régulation parfois très complexes. Or, pouvoir analyser le comportement
d'un réseau génique est indispensable pour comprendre les interactions
entre protéines et leurs fonctions. Il existe plusieurs approches et
outils pour modéliser puis analyser les réseaux géniques dans un cadre
formel, comme les systèmes de fonctions booléennes et les systèmes
hybrides. Or, la plupart des algorithmes d'analyse mettent le modèle "à
plat" sans exploiter la modularité du problème. Nous avons proposé,
implémenté et expérimenté une approche modulaire de modélisation et
analyse qui utilise une discrétisation basée sur les inclusions
différentielles de Filippov. Cette approche permet de vérifier
efficacement des propriétés du modèle d'un réseau génique, comme
l'atteignabilité d'un état. Cependant, le cadre ne tient compte que des
interactions entre protéines, à une même échelle de temps.
L'objectif de ce projet est de
- faire un travail bibliographique sur les méthodes d'analyse modulaire
des réseaux géniques,
- apporter des généralisations mathématiquement bien fondées au cadre de
modélisation et vérification modulaires des réseaux géniques, par
exemple pour tenir compte de différentes échelles de temps,
- si le temps le permet, identifier les problèmes liés à la modélisation
hétérogène qui permette de prendre en compte conjointement un réseau
génique et son interaction avec un modèle du métabolisme de la cellule,
et proposer des éléments de réponse,
- explorer l'approche choisie à l'aide d'études de cas.
URL sujet détaillé : http://pop-art.inrialpes.fr/Stages/l3.html
Remarques : Co-encadrant : Hidde DE JONG, projet HELIX.
|
|
|
|
|
|
Aline PARREAU : SL306-24 Vulgariser la démarche scientifique en mathématique en donnant accès à des questions proches de la recherche actuelle.
|
|
|
Description
|
|
Le but de ce stage est de réaliser une situation proche d'un problème de la recherche actuelle en mathématique discrète, qui pourra être proposé à tout public et, en particulier, en classe sous forme d'un atelier " maths à modeler ".
Dans un premier temps, le stagiaire devra étudier un problème de parcours (Hamiltonien) dans une structure discrète (de type grille). Le problème de décision associé est connu pour être NP-complet [1] ; cependant pour certaines restrictions, on peut espérer le résoudre efficacement. Si les résultats obtenus apparaissent significatifs par rapport à l'état de l'art, ils pourront être valorisés en terme de publication dans une revue du domaine.
La résolution partielle de ces problèmes permettra de déterminer certaines étapes accessibles au plus grand nombre. On souhaite réinvestir cette analyse en vue de la réalisation d'un support matériel (jeu / casse-tête) permettant à l'utilisateur d'entrer dans une démarche de résolution proche de celle du chercheur. Une réalisation informatique sous forme d'applet java pourra compléter le travail et s'intègrera dans notre site
http://www-leibniz.imag.fr/LAVALISE
où l'on propose plusieurs situations de ce type.
Selon les résultats obtenus, nous proposerons un sujet de recherche similaire à un groupe d'élèves de collège et/ou de lycée à la rentrée prochaine sous forme d'une action " maths en jeans ". Le travail de ce groupe permettra d'affiner l'analyse préalable et pourra servir de base pour la conception d'un atelier " maths à modeler ". Un tel atelier consiste en la mise en place de 4 à 6 séances de recherche proposées à des élèves d'école primaire jusqu'au lycée.
Pour une bonne compréhension de l'approche " maths à modeler ", on proposera, en début de stage, au stagiaire de co-animer une séance ponctuelle (2-3 heures) dans une classe d'école primaire des environs de Grenoble. Cette séance a pour but de sensibiliser les élèves à la démarche de recherche à travers plusieurs des situations existantes dans le cadre de notre projet. Le stagiaire se familiarisera ainsi avec notre approche.
[1] - A. Itai, C.H. Papadimitriou, J. Szwarcfiter. Hamilton paths in grid graphs. SIAM Journal on Computing 11 (2000), pp. 7-28.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL306-25 Décomposition automatique d'un modèle 3D de personnage pour l'animation
|
|
|
Description
|
|
Contexte :
Lorsqu'on souhaite animer un modèle 3D de personnage (par exemple pour un jeu vidéo ou un film d'animation), la méthode actuellement la plus utilisée consiste à créer une hiérarchie des articulations du personnage, appelée "squelette d'animation", à déplacer ces articulations puis à déformer le modèle autour de celles-ci. Afin d'obtenir une animation réaliste, il faut savoir exactement quelles articulations influencent quelles parties du modèle. Pour l'instant, ceci est fait automatiquement, par simples interpolations linéaires ... ce qui conduit à des artefacts qu'il faut ensuite corriger à la main.
Les laboratoires GRAVIR (informatique graphique) et LMC (mathématiques appliquées) travaillent conjointement sur un projet visant à proposer des
outils plus évolués pour obtenir une animation plus réaliste. Dans ce cadre, nous souhaitons développer une méthode de décomposition automatique du modèle 3D d'un personnage (représenté par une surface maillée) en régions
anatomiquement pertinentes : bras, avant-bras, mains, jambes, ... Ces régions devront se chevaucher au niveau des articulations (coudes, poignets, genoux, ...), pour permettre une déformation du modèle plus efficace.
Objectifs :
Le stage débutera par une étude bibliographique des méthodes existantes de décomposition automatique de maillages en régions sémantiquement pertinentes.
Le stagiaire évaluera ensuite si une de ces méthodes peut être adaptée afin d'obtenir des régions se chevauchant et intéressantes pour notre application. Il proposera éventuellement une méthode originale, par exemple basée sur le
squelette d'animation qui donne des informations précieuses sur la position des articulations. Cette méthode pourra faire l'objet d'une implémentation en C++ si le stagiaire est motivé.
URL sujet détaillé : http://www-evasion.imag.fr/Membres/Franck.Hetroy/Students/sujet_l3-2.html
Remarques : Le stage sera co-encadré par Boris Thibert du laboratoire LMC-IMAG (http://www-lmc.imag.fr/lmc-mga/Boris.Thibert/). Une partie du stage pourra s'effectuer au LMC, sur le campus de Grenoble, et l'autre à GRAVIR, situé à l'INRIA de Grenoble.
|
|
|
|
|
|
Benjamin COHEN : SL306-26 Conception, analyse et implémentation d'algorithmes pour la simulation de réseaux de neurones impulsionnels
|
|
|
Description
|
|
Les neurones sont des cellules qui communiquent entre elles par le biais d'impulsions électriques stéréotypées, et peuvent donc être modélisés comme des systèmes à événements discrets. Les neurosciences computationnelles reposent sur la simulation de grands réseaux de neurones, qui nécessite le développement d'algorithmes efficaces. Cela pose d'intéressants problèmes d'algorithmique, autour notamment des structures de files de priorité (priority queues) pour gérer les événements (impulsions).
Il s'agira pour l'étudiant d'explorer un certain nombre d'idées algorithmiques pour la simulation de réseaux de neurones impulsionnels. Le travail comportera une partie théorique (conception et analyse des algorithmes et des structures de données) et pratique (implémentation et test d'un réseau de neurones).
Le stage sera effectué au sein du projet Odyssée (INRIA/ENS) à l'Ecole Normale Supérieure de Paris.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Florian HATTAT : SL306-27 formalisation d'ensembles dénombrables en Coq
|
|
|
Description
|
|
Il s'agit de formaliser en Coq la notion d'ensemble
au plus dénombrable.
Coq est un système d(aide à la démonstration basé
sur le calcul des constructions inductives.
Le travail fourni devra être compatible avec les
bibliothèques sur les ensembles déjà existantes
et pouvoir être utilisé dans le travail actuel de
l'encadrant.
URL sujet détaillé : http://www.labri.fr/~casteran/stageLyon.pdf
Remarques :
|
|
|
|
|
|
SL306-28 Théorie des Jeux, Algorithmique et Aspects Dynamiques
|
|
|
Description
|
|
Domaine du stage:
La complexité d\'un algorithme est généralement évaluée au pire
des cas (éventuellement en moyenne). Cela revient à évaluer
l\'algorithme vis-à-vis d\'une certaine notion d\'adversaire, qui cherche
systématiquement le pire cas, mais en supposant généralement que tous
les agents participants sont en coalition contre cet adversaire.
Cette étude est insuffisante pour nombres d\'algorithmes distribués: souvent, chacun des partenaires est en fait aussi en
compétition contre les autres participants.
On cherche alors à discuter les propriétés de l\'algorithme, en
utilisant les outils de cette théorie: par exemple, à discuter vers quelles situations peuvent converger les partenaires, ou quelles sont les garanties de sécurité globales sur l\'algorithme.
Depuis quelques années, de plus en plus de travaux de la littérature explorent ces directions.
Description détaillée du travail:
La théorie des jeux vise à décrire les
situations d\'équilibre(s).
Elle ne permet pas à priori de discuter des
aspects dynamiques: comment évolue un système avant d\'atteindre un
certain équilibre (si équilibre il y a).
Par exemple, il est important de déterminer comment évolue une
``négociation\'\' entre partenaires concurrents (comment ``réagit\'\' un
partenaire aux réponses des autres partenaires), pour comprendre le
comportement dynamique d\'un algorithme.
Il existe des outils pour cela, comme la théorie des jeux répétés,
ou la théorie des jeux évolutionnaire.
L\'objectif du stage est de contribuer à comprendre les différents
modèles existants du dynamisme, et les propriétés que l\'on peut
établir sur ces modèles.
On cherchera à appliquer les résultats sur des problèmes simples tirés
de problèmes algorithmiques liés aux télécommunications.
URL sujet détaillé : http://www.loria.fr/~bournez/load/sujet-l3-2006.pdf
Remarques : Coencadrement avec Johanne Cohen, CR CNRS.
Possibilité de rémunération: oui.
|
|
|
|
|
|
SL306-29 Algorithmes d'approximation pour le calcul de l'axe médian optimal
|
|
|
Description
|
|
--Contexte--
En analyse d'images, pour analyser une forme 2D ou 3D, on effectue
très souvent une décomposition préalable de la forme en éléments plus
simples selon des critères géométriques ou topologiques.
En géométrie discrète ou en géométrie algorithmique, on utilise
souvent l'axe médian (ou squelette) comme outil de décomposition
géométrique. Cet axe médian correspond en fait à une décomposition de
la forme en un nombre minimal de disques ou de boules (axe
médian=centre des boules maximales). Bien évidemment, cette
décomposition est réversible puisque l'union des disques ou des boules
doit permettre de retrouver la forme originale. Quelle que soit la
dimension, des algorithmes optimaux en temps existent pour extraire
les centres des boules maximales, c'est à dire les boules qui ne sont
pas couverte par aucune autre boule. Cet axe médian n'est pas minimal
en nombre de boules car nous n'avons pas traité les couvertures d'une
boule par une union d'autres boules.
Lorsque l'on souhaite avoir un axe médian optimal en nombre de boules,
nous obtenons un problème de couverture NP difficile. Le contexte du
stage est donc l'analyse d'algorithmes rapides d'approximation de cet
ensemble optimal.
--Objectifs--
Il s'agit donc de mettre en place des algorithmes d'approximation de
ce problème NP avec, autant que possible, une borne sur la qualité de
l'approximation. (distance entre la solution de l'algorithme et la
solution "optimale").
Dans une première phase, une étude de la bibliographie sur le sujet
devra être menée en collaboration avec les membres de l'équipe.
Le stage s'effectuera au laboratoire LIRIS (Campus de la Doua) dans
l'équipe "Modèles discrets et multirésolutions" de l'axe "Images et
vidéos".
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL306-30 Algorithme garanti de segmentation de surfaces d'objets discrets.
|
|
|
Description
|
|
Les objets 3D auxquels nous nous intéressons ici sont des ensembles de
points (appelés voxels, par analogie avec le terme pixel) placés sur
une grille régulière. Ce type de données apparaît dès lors qu'une
acquisition par capteurs numériques est effectuée sur un objet, ou
bien dans le domaine médical par exemple, où les données fournies par
un IRM ou un scanner X sont interprétées sous cette forme.
Ces données, décrites par un ensembles de cubes sur la grille unitaire portent
une information très redondante et inexploitée : leur géométrie. En effet, la
représentation de la surface d'un cube de côté n dans l'espace discret nécessite
O(n²) voxels, alors que la représentation de son analogue polyédrique ne
nécessite que 6 faces quelque soit n. Il paraît donc intéressant (dans un objectif de
compression et/ou de modélisation) de s'intéresser à la géométrie
de la surface de ces objets, en exploitant par exemple la coplanarité
d'ensembles de voxels de surface.
Il existe aujourd'hui de nombreux algorithmes de reconnaissance d'un plan
discret (ensemble de voxel coplanaires au sens discret), permettant de décider
si un ensemble de voxels est un morceau de plan, et le cas échéant de donner les
paramètres de ce plan.
L'application d'un algorithme de reconnaissance sur la surface d'un objet
discret afin de la découper en morceaux coplanaires est appelée segmentation. Nous
avons montré récemment que la segmentation d'une surface discrète en un nombre
minimal de morceaux de plans est un problème NP-complet, et se pose donc
maintenant le problème de la définition d'algorithmes d'approximation garantis.
Le travail demandé dans ce stage concerne la définition et la mise en oeuvre
d'un algorithme de segmentation avec une garantie sur la minimalité du nombre de
plans reconnus. Cet algorithme s'inspirera des algorithmes garantis pour
d'autres problèmes NP-complets de couverture/partition de graphes ou
d'ensembles.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL306-31 Parallel Tree Skeletons in Bulk Synchronous Parallel ML
|
|
|
Description
|
|
Les squelettes algorithmes d'arbres sont des fonctions d'ordre supérieur proposées par la bibliothèque SkeTo (http://www.ipl.t.u-tokyo.ac.jp/sketo/) développées en C++ pour la manipulation d'arbres sur machines parallèles.
La plupart des bibliothèques de programmation parallèle par squelettes algorithmiques offrent en général des fonctions sur des structures de données régulières. La bibliothèque SkeTo est donc originale de ce point de vue.
Notre langage Bulk Synchronous Parallel ML ou BSML (cf premier séminaire des élèves de 2005-2005) permet la programmation parallèle d'algorithmes Bulk Synchronous Parallel ML avec Objective Caml.
L'objectif du travail est de réaliser une implantation en BSML de squelettes algorithmiques sur les arbres, inspirée par SkeTo (il faut donc déjà comprendre les principes puis l'implantation de SkeTo). Les algorithmes de SkeTo ne sont pas des algorithmes BSP, il faudra donc adapter certains de ces algorithmes. La partie la plus difficile à implanter sera la répartition des arbres. Le reste sera plus directement traduisible depuis SkeTo.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Omar FAWZI : SL306-32 Mise en gage quantique
|
|
|
Description
|
|
Contrairement au calcul quantique qui nécessite la construction hypothétique d'un ordinateur quantique, les protocoles quantiques cryptographiques développés peuvent déjà être concrètement utilisés.
Malgré cela, le nombres de protocoles utilisant leur supériorité quantique pour assurer leur sécurité inconditionnelle (ce qui n'a pas d'équivalent en cryptographie traditionnelle) reste faible.
Depuis le protocole de distribution de clés secrètes de Bennett et Brassard en 1984, les résultats sont plutôt négatifs. Il est impossible, même quantiquement, de développer des protocoles inconditionnellement sûrs pour la mise en gage de bit (l'équivalent du coffre-fort à distance),
et ses extensions : le tirage à pile ou face à distance et l'élection aléatoire à distance
Cependant, récemment de nouvelles avancées viennent contrebalancer ces résultats négatifs. Par exemple, il est possible de garantir un biais borné dans le tirage à pile ou face et dans l'élection, il est possible de mettre en gage un bit si un troisième participant vient prendre place.
Le stage consistera en l'étude des résultats négatifs et positifs, d'en faire une synthèse, de compléter les preuves manquantes, et éventuellement d'effectuer des simulations numériques là où les résultats théoriques sont inconnus.
Les articles de référence sont
- Defeating classical bit commitments with a quantum computer. Gilles Brassard, Claude Crépeau, Dominic Mayers, Louis Salvail. http://arxiv.org/abs/quant-ph/9806031
- Classical and quantum strategies for two-prover bit commitments. Claude Crépeau, Jean-Raymond Simard, Alain Tapp. http://crypto.cs.mcgill.ca/~crepeau/QIP06-NB.pdf
- Lower bound for a class of weak quantum coin flipping protocols. Andris Ambainis. http://arxiv.org/abs/quant-ph/0204063
- A large family of quantum weak coin-flipping protocols. Carlos Mochon. http://arxiv.org/abs/quant-ph/0502068
- Quantum coin-flipping. Alexei Kitaev. http://www.msri.org/publications/ln/msri/2002/qip/kitaev/1/index.html
URL sujet détaillé :
:
Remarques : Le stage se prolongera sans doute jusqu'au 31 juillet.
|
|
|
|
|
|
SL306-33 Sur la notion de flot d'information sûr.
|
|
|
Description
|
|
Ce stage propose d'étudier la formalisation de la notion de flot d'information, notion qui est utilisée dans la certification de programme par typage. Intuitivement, la propriété à garantir est qu'un programme n'implante pas de transfert d'une information secrète vers un résultat qui peut être consulté publiquement. Cette idée est habituellement formalisée dans la propriété dite de "non-interférence", et de nombreuses études montrent que, pour des langages de programmation variés, on peut construire un système de typage des programmes qui garantit cette propriété.
Toutefois, la "non-interférence" n'est pas très facile à manipuler, parce que c'est une propriété qui compare différents calculs d'un programme, partant d'états mémoire différant dans leur partie "secrète". Dans un travail récent [1] nous avons proposé une formalisation directe de la notion de flot d'information réalisé par un programme (le langage de programmation étant le coeur fonctionnel et impératif de ML). Pour ce faire, nous utilisons une machine abstraite, qui "propage" le niveau de confidentialité des valeurs calculées et mises en mémoire au cours de l'exécution du programme. Nous pouvons alors définir une "erreur de sécurité" comme une situation où l'on place en mémoire, à une adresse publiquement accessible, une valeur dont le niveau de confidentialité est "secret", et nous disons qu'un programme est sûr s'il ne conduit pas à de telles erreurs à l'exécution. La propriété de sûreté se présente ainsi, de manière tout à fait classique, comme une propriété de "safety" - pas d'erreur à l'exécution.
Nous avons montré qu'un système de type conçu pour garantir la "non-interférence" garantit aussi l'absence d'erreur à l'exécution. Mais il reste de nombreuses questions à résoudre, par exemple :
- est-ce que l'absence d'erreur à l'exécution implique la propriété de "non-interférence" ? Plus généralement, quelle est exactement la relation de la notion de sûreté proposée avec la "non-interférence" ?
- peut-on de la même manière traiter les "fuites à la terminaison", par lesquelles on peut indirectement acquérir de la connaissance sur les données secrètes d'un programme ?
- peut-on incorporer dans ce traitement les constructions de "déclassification", indispensables dans la pratique ?
Le but du stage est d'aborder - et peut-être résoudre - quelques unes de ces questions. Il faudra au préalable se familiariser avec les travaux de recherche dans le domaine de la sécurité des programmes (qui est l'objet de nombreuses conférences actuellement), et plus particulièrement en ce qui concerne l'analyse statique, par typage, du flot d'information.
[1] G. Boudol, Secure information flow as a safety property, to appear (2006).
URL sujet détaillé :
:
Remarques : Une rémunération du stage est possible, pour compenser le coût d'un séjour sur la Côte d'Azur.
|
|
|
|
|
|
SL306-34 Abstract geometrical computation -- machines à signaux
|
|
|
Description
|
|
Le 22 février 2006, au séminaire des élèves nous avons présenté les machines à signaux, les beaux dessins qu'elles engendrent et montrer que l'on peut y mener des calculs au sens classique mais aussi, grâce à une judicieuse utilisation des accumulations, mener des calculs sortant du cadre classique de la calculabilité puisque l'arrêt d'un machine de Turing peut être décidé.
Divers sujets sont disponibles dans ce contexte, chacun pouvant être plus ou moins développé:
[Accumulation non rationnelle] En partant d'un contexte où seuls les nombres rationnels sont utilisés, il doit être possible de faire une accumulation avec des coordonnées irrationnelles.
Le but du stage pourrait être la construction d'un tel exemple en utilisant de petits systèmes de réécriture (p.e. suite sturmienne ou engendrée comme point fixe d'une grammaire non-contextuelle).
On peut aller plus loin en cherchant à systématiser la méthode pour toute une classe de constructeur d'irrationnels ou carrément de tous les réels récursifs.
[Liens avec d'autre modèles] À la base, les seules opérations utilisés sont l'addition, la soustraction, la multiplication, la division et la comparaison entre rationnels. Dans quelle mesure, les machines à signaux correspondrait-elles à un modèle de calcul type assembleur (ou machine RAM) sur les rationnels avec les primitives correspondantes?
[Liens avec les ordinaux] Il est possible de définir des ",continuations," après une accumulation et par delà des accumulations de tout ordre. Il est possible de caractériser le degré d'une accumulation par un ordinal.
Quels sont les ordinaux que l'on peut atteindre?
URL sujet détaillé : http://www.univ-orleans.fr/lifo/Members/Jerome.Durand-Lose/Recherche/Sujets/06/MIM/fiche_stage_AGC.pdf
Remarques :
|
|
|
|
|
|
SL306-35 Motifs et dynamique dans les éboulements de tas de sable unidimensionnels
|
|
|
Description
|
|
Différentes variations du modèle séquentiel du tas de sable ont été étudiées. Étrangement, le cas parallèle n'est que peu étudié. Le sujet du stage est de partir d'un modèle simpliste très bien compris et de le généraliser.
Un tas de sable unidimensionnel se modélise par une suite de sites contenant chacun un nombre fini de grains. Ce système évolue en suivant la dynamique suivante : chaque site regarde s'il a au moins 2 grains, si c'est le cas, il en envoie un à chacun de ses voisins. Tous les sites sont mis à jour simultanément.
On voit apparaître différents motifs (par exemple "...22222..." ou "...3131..." qui alterne avec "...1313..."). Les frontières entre ces motifs forment des segments de droites discrètes ou signaux. La dynamique du tas de sable est complètement déterminée par les collisions entre ces signaux. Tout cela est illustré par la figure sur le site web.
La généralisation proposée dans ce stage est de paramétrer la dynamique de la façon suivante:
"chaque site regarde s'il a au moins , si c'est le cas, il en envoie chacun de ses voisins". D'autres motifs et signaux apparaissent en fonction de
Le but du stage est de pouvoir engendrer et caractériser rapidement les motifs et signaux en fonction des paramètres et de regarder comment ils varient en fonction des paramètres.
Par exemple, il doit y avoir des effets de passage à l'échelle: en multipliant le nombre de chaque pile par 2 et en remplaçant 502 80 79 81 502s,e) 502 80 79 81 5022s,2e) il se passe la même chose.
URL sujet détaillé : http://www.univ-orleans.fr/lifo/Members/Jerome.Durand-Lose/Recherche/Sujets/06/MIM/fiche_stage_CFG.pdf
Remarques :
|
|
|
|
|
|
SL306-36 Automates finis et fonctions du continu dans un alphabet fini
|
|
|
Description
|
|
Depuis les début de la théorie des langages et le théorème de extsc{Kleene}, les chercheurs n'ont eu de cesse de proposer des extensions, e.g.: lettres permutables (traces), lettres datées (mots temporisés) ou sur des supports partiellement ordonnés ou infinis. Ces modèles ne sortent que ponctuellement du cadre discret; l'utilisation de la continuité n'est que très parcimonieuse, pour des passages à la limite : à l'infini, pour un ordinal limite, certaines coupes d'un ordredots
Nous tentons de franchir le pas en essayant d'élaborer une théorie des langages pour des " mots " qui sont des fonctions de 5.0080040,1[ un alphabet fini. On ne peut formuler de critère direct de reconnaissance par un automate fini. Pour remédier à cela, nous approximons une fonction en découpant 5.0080040,1[ une suite d'intervalles tels que pour chacun d'eux si la fonction n'y est pas constante, alors la longueur de l'intervalle est inférieur à un varepsiloné. À partir de ce découpage, on construit une suite de lettres (sur un alphabet plus grand) correspondant aux valeurs atteintes sur l'intervalle. Nous nommons ce mot une varepsilon0approximation de la fonction. La reconnaissance par un automate correspond alors à avoir, pour tout varepsilon une varepsilon0approximation de la fonction est reconnue par l'automate.
Parmi les premiers résultats connus citons l'indiscernabilité de certaines fonctions ce qui amène à une notion de classe, l'existence de classes correspondant à des fractales, la non-cloture par complémentarité, des problèmes avec la concaténation, certaines classes ne peuvent être reconnues seules...
Le but du stage est d'explorer ce monde qui touche d'une part à la théorie des langages, classique et discrète, et de l'autre aux bases de l'analyse
(présentes par le forallvarepsilon502 80 79 81 502. Parmi les directions que l'on peut envisager (et dont des réponses définitives peuvent dépasser le cadre du stage) :
- autre définition des classes et liens entre elles,
- opérateurs sur les (ensembles) de classes et opérateurs sur les automates,
- description des classes reconnues par un automate, construction d'automates en fonction de descriptions (d'ensembles) de classes, et forme de théorème de extsc{Kleene}.
URL sujet détaillé : http://www.univ-orleans.fr/lifo/Members/Jerome.Durand-Lose/Recherche/Sujets/06/MIM/jdl-FunctionAutomata.pdf
Remarques :
|
|
|
|
|
|
SL306-37 A distributed coding scheme for image compression
|
|
|
Description
|
|
In classical compression techniques for multimedia, specially still images, the encoder exploits the statistical spatial correlation of the image at the encoder and compresses it close to the theoretical limits using arithmetic coding; afterwards the function of the decoder is much simpler than the encoder. This approach works pretty well for encoding once at the server and decoding many times at the clients. However for encoding on low-power handhelds, the encoder complexity has to be shifted to the decoder side.
In this internship, we will develop a coding scheme for image and video using distributed coding principles. Error correcting codes will be applied and a series of experiments will be done using synthetic and natural image sequences. The project will deal with both theoretical and practical aspects of the Distributed Source Coding.
Keywords: Error correcting codes, information theory, distributed source coding
URL sujet détaillé :
:
Remarques : Co-advisors: Khalid IDRISSI, Cagatay DIKICI
|
|
|
|
|
|
Adrien PANHALEUX : SL306-38 Modèle de la main pour une préhension interactive
|
|
|
Description
|
|
Dans le cadre de la recherche sur l'amélioration des périphériques pour interagir avec un ordinateur, de nombreux travaux se sont orientés vers des dispositifs à retour d'effort adaptés à la main. Ces dispositifs ont cherché à reproduire de manière virtuelle l'intéraction naturelle d'une personne avec son environnement par l'intermédiaire de ses mains. Aujourd'hui, les dispositifs proposés sont lourds et n'apparaissent pas pertinents. Cela pose la question de la connaissance et de la modélisation de la main.
L'objectif de ce projet de recherche est de modéliser et calculer une main virtuelle capable de reproduire la plupart des situations de préhension de manière interactive. Ce premier modèle aura déjà des applications pratiques pour agir et collaborer de manière plus naturelle dans un environnement virtuel. Le projet sera développé dans SOFA, une plate-forme de simulation orienté médical.
Dans ce projet, le modèle mécanique de la main sera basé sur un squelette pour les mouvements globaux de la paume et des doigts. Le squelette sera modélisé par des poutres. Il sera complété de déformations locales au niveau des coussinets à partir des caractéristiques bio-mécaniques connues dans la littérature.
Pendant le stage, l'étudiant travaillera sur la modélisation géométrique et bio-mécanique de la main. A partir d'un modèle en triangle texturé, il proposera des lois cinématiques pour animer la peau en fonction des mouvements du squelette. Ensuite, ce modèles sera complété par le calcul des déformations locales au niveau des coussinets. Une première expérimentation en 2D a déjà permis de dégager des résultats satisfaisants. Ils seront une base de départ pour l'étudiant.
URL sujet détaillé :
:
Remarques : Il a été convenu qu'Adrien Panhaleux prendrait ce stage.
|
|
|
|
|
|
SL306-39 Visualisation stéréoscopique de surfaces triangulaires
|
|
|
Description
|
|
La discipline de la Conception Géomtrique Assiste par Ordinateur (CGAO) fournit
les algorithmes nécessaires pour la représentation de courbes et de surfaces sur
un ordinateur en se basant sur des méthodes de mathématiques appliquées et
d'informatique. Cette discipline est apparue pour répondre l'importance croissante
des ordinateurs dans les processus industriels et aux besoins d'applications dans
les domaines de l'industrie automobile, aronautique et mécanique ainsi qu'en
architecture et en médecine. Elle est la base des logiciels modernes de CAO
(Conception Assiste par Ordinateur), qui mettent la disposition des utilisateurs
les moyens de repérsentation, de construction, de manipulation et de visualisation
d'objets tridimensionnels sur un ordinateur en vue de fournir des résultats satisfaisants
au regard des critères de fabrication. La CAO est un domaine interdisciplinaire
organisé autour du noyau géomtrique-mathématique qui exige la collaboration entre
les mathématiques, l'informatique et la mécanique. Il s'agit aussi d'une importante
branche industrielle dans le monde entier et en particulier en France : chaque année,
Paris le plus grand salon international de la CAO, le MICAD, rassemble les plus
grandes sociétés mondiales de ce domaine. En matire de recherche, tous les 4 ans,
a lieu en France, un congrès internationale réunissant des centaines de
chercheurs qui présentent leurs résultats concernant la modélisation géometrique de
courbes et de surfaces.
De nouvelles formes d'interactions entre le
constructeur et le logiciel de CAO, plus naturelles que l'interaction courante
travers le clavier et la souris sont en train d'être etudies. De telles interfaces,
comme par exemple des écrans stéréoscopiques et des gants virtuels,
ont été développes dans le domaine moderne de
la réalité virtuelle, qui représente la simulation sur ordinateur d'un environnement
dans lequel des objets et des phénomènes virtuels, sont présents de façon à donner
l'impression d'être réels.Un ou plusieurs utilisateurs se trouvent l'intérieur
d'un environnement 3D simulé,créé et géré dynamiquement par l'ordinateur.
A travers des dispositifs appropriés,ils peuvent interagir avec cet environnement
tout en recevant l'illusion d'un mouvement et d'une immersion spatiale effective.
Ce projet s'intresse l'étude des liens possibles entre la CGAO d'une part et
la réalité virtuelle d'autre part.
Il s'agit de participer au développement d'algorithmes et de programmes
informatiques afin de permettre la modlisation gomtrique de courbes et de surfaces
en ralit virtuelle.
En particulier, il sera demande d'implémenter un algorithme pour la représentation
de surfaces triangulaires sur des quadriques (par exemples, sphères, paraboloides,...),
voir http://www.univ-valenciennes.fr/macs/caomacs/quadric_const.htm,
et de visualiser ces surfaces en stéréovision.
Le travail sera effectue en collaboration avec un étudiant mathématicien
stagiaire (niveau master 1).
Programme de travail :
- étude de la configuration existante (écran Stéréo 3D Barco, SGI Octane2, PC)
- familiarisation avec des bases en OpenGL, ainsi qu'avec la représentation
Bézier de courbes et de surfaces.
- programmation d'une interface graphique pour la représentation de courbes et
de surfaces en forme Bézier.
- implmentation d'un algorithme pour la représentation de surfaces
triangulaires, visualisation sur l'écran Barco en stéréovision.
Bases necessaires :
- Programmation orientée objet en C++
- Algèbre linéaire et géométrie analytique, Analyse (généralement acquis
en classes préparatoires).
URL sujet détaillé :
:
Remarques : Travail en équipe avec un étudiant mathématicien
en master 1.
|
|
|
|
|
|
SL306-40 Un modeleur géométrique pour l'interprète mathemagix.
|
|
|
Description
|
|
Pour beaucoup de problèmes pratiques, la résolution est un processus long et
souvent complexe combinant un ensemble d'outils aussi nombreux que variés,
allant du calcul symbolique ou numérique à la visualisation de résultats.
Dans le projet GALAAD, nous nous intéressons plus particulièrement à l'interaction entre algèbre et géométrie et nous avons développé des outils
spécialisés pour la modélisation géométrique, s'appuyant sur des solveurs algébriques.
Afin de faciliter l'utilisation de ces implémentations en C++ (bibliothèque
logicielle synaps http://www-sop.inria.fr/galaad/logiciels/synaps/), nous travaillons actuellement sur leur connection avec l'interprète mathemagix
(http://www.mathemagix.org/mmxweb/web/welcome.en.html)
typé, polymorphe et générique. Pour cela, nous avons mis en place un mécanisme automatique
de liaison d'un code C++ externe à cet environnement, qui procède de la façon suivante:
* Spécification du "dictionnaire" entre les types et fonctions de l'interprète
et ceux du code C++ externe.
* Analyse et génération automatique d'un code de liaison
* Compilation et production d'une librairie qui sera chargée dynamiquement dans l'interprète.
Un des intérêts de l'approche est donc de rendre modulaires et facilement
utilisables des outils performants, dédiés à un domaine d'application spécifique.
L'objectif du travail proposé est d'appliquer cette démarche afin de
connecter un modeleur algébrique-géométrique que nous développons, avec l'interprète
mathemagix. Il s'agira donc de pouvoir piloter l'outil de visualisation à partir de mathemagix, tout en contribuant à un projet Open Source en lui apportant un outil de modélisation géométrique.
Ce travail permettra à travers l'utilisation effective de différents outils, de se
familiariser avec les domaines du graphisme, du calcul symbolique-numérique,
du typage et de la programmation générique.
URL sujet détaillé :
:
Remarques : Possibilité de rénumération.
Co-encardrement: J. Wintz pour le modeleur géométrique
|
|
|
|
|
|
SL306-41 Résolution de la logique de Presburger par élimination de quantificateur
|
|
|
Description
|
|
Décrire l'ensemble des solutions entières à une contrainte linéaire de la forme 2.x+3.y=1 est un problème assez facile. Il suffit en effet de calculer des coefficients de Bézout pour en déduire qu'un couple (x,y) est solution de 2.x+3.y=1 si et seulement si il existe p tel que x=3.p+5 et y=-2.p-3. Le problème réciproque qui consiste à trouver la contrainte linéaire 2.x+3.y=1 à partir de la formule "il existe p tel que x=3.p+5 et y=-2.p-3" est un cas particulier du problème appelé l'élimination de quantificateur dans la logique de Presburger (dans notre exemple, on souhaite éliminer le quantificateur "il existe p tel que").
La logique de Presburger correspond intuitivement à toutes les formules linéaires que l'on peut écrire à partir de contraintes linéaires a_1.x_1+...+a_n.x_n=c ou a_1.x_1+...+a_n.x_n<c où les a_i et c sont des constantes entières, des conjonctions et disjonctions de formules, des quantifications existentielles "il existe p tel que" et universelles "pour tout p on a".
Différents algorithmes ont été proposés pour décider si une formules de Presburger admet au moins une solution: par des automates, par des semi-linéaires, ou encore par élimination de quantificateurs implémentés dans l'outil Omega.
L'objectif du stage est d'étudier les différentes méthodes connues pour éliminer les quantificateurs dans la logique de Presburger et d'implémenter en C une de ces méthodes.
URL sujet détaillé : http://www.labri.fr/perso/leroux/encadrement/stage_ENS_Lyon_2006.ps
Remarques :
|
|
|
|
|
|
SL306-42 Une approche pyramidale pour la segmentation de documents graphiques
|
|
|
Description
|
|
Le projet Qgar du LORIA travaille sur la reconnaissance de documents
graphiques. La "binarisation" consiste à séparer les objets (texte et graphique)
du fond de l'image d'un document, en transformant l'image initiale à niveaux de
gris en une image binaire. C'est une tâche très complexe, à cause du bruit
introduit par le processus de numérisation (scanner, typiquement) et à cause du
fait que certaines (petites) parties textuelles sont collées aux composantes
graphiques (de taille beaucoup plus grande). Le travail demandé consiste à
adapter l'approche mixte de T. Gadi et al. aux documents graphiques, en
utilisant une structure pyramidale plus souple pour découper l'image et en
adoptant des tests statistiques robustes pour la condition d'arrêt du
découpage.
URL sujet détaillé : http://qgar.loria.fr/stages.php
Remarques : - possibilité de rémunération
- Gérald Masini coencadrant
|
|
|
|
|
|
Chaddai FOUCHE : SL306-43 Automates pour l'analyse et le traitement de documents compressés
|
|
|
Description
|
|
Les documents semi-structurés, tels que dans XML, sont souvent analysés à l'aide d'automates
d'arbres. Si un document t est compressé -- i.e., sa structure n'est plus celle d'un arbre mais d'un dag --, il est néanmoins possible (sans devoir décompresser t) de se servir de ces automates,
pour décider si t est conforme à une
spécification, et pour l'évaluation des
requêtes (positives) du format Core XPath
sur t. En effet :
i) La notion de run des automates d'arbres peut être adaptée de manière qu'ils puissent courir directement sur des dags ou des arbres. Cette
adpatation ne modifie pas la notion usuelle
de run sur les arbres.
ii) A chaque requête Q sur un axe Core XPath de base, peut être associé un automate A de mots; il est destiné à courir soit sur le dag de
dépendance de la grammaire d'arbre régulière (``straightline'' et normalisée) déterminée
par le document, soit sur les haies (hedges) de cette grammaire. Les états de l'automate sont des paires sémantiques qui reflètent le fait de la
sélection ou non (par Q) du noeud traversé par le run de A, ou le fait que ce noeud soit ou non sur un chemin vers un noeud sélectionné par Q. Des règles de priorité sur les paires, définies de manière globale et indépendammant de l'axe, permettent de construire de façon unique un run de A qui retournera, en une seule passe top-down,
les réponses à la requête Q sur le documen
donné.
Le travail à réaliser lors du présent stage peut être résumé comme suit :
- Se familiariser avec les notions de document XML, et la notion de requêtes sur de tels documents, et plus particulièrement celles du format (Core) XPath.
- Se familiariser avec les notions d'automates d'arbres, de grammaire d'arbres, et les manières
de traduire une requête comme un automate.
- Proposer un programme en JAVA, implémentant l'algorithme qui construit le run unique (de priorité maximale) de l'automate A sus-mentionné, sur un document donné quelconque (compressé ou non).
Contact(s)} :
Siva Anantharaman (LIFO),
mail : siva-orleans.fr
Barbara Fila (LIFO),
mail : fila-orleans.fr
Références Biblio :
[1] P.~Buneman, M.~Grohe, C.~Koch,
``Path queries on compressed XML''.
In Proc. of the th. on VLDB, 2003,
pp. 141-152, Ed. Morgan Kaufmann.
[2] G.~Busatto, M.~Lohrey, S.~Maneth,
``Grammar-Based Tree Compression'',
EPFL Technical Report IC/2004/80,
http://icwww.epfl.ch/publications.
[3] G.~Busatto, M.~Lohrey, S.~Maneth,
``Efficient Memory Representation of
XML Documents'', In Proc. DBPL'05, LNCS 3774,
Springer-Verlag, 2005.
[4] B.~Fila, S.~Anantharaman,
``Automata for Analyzing and Querying Compressed
Documents'', Research Report, RR-2006-03, LIFO,
http://www.univ-orleans.fr/lifo/prodsci/rapports/, March 2006.
[5] M.~Frick, M.~Grohe, C.~Koch,
``Query Evaluation of Compressed Trees'',
In Proc. of LICS'03, IEEE, pp. 188--197, 2003.
[6] G.~Gottlob, C.~Koch, R.~Pichler, L.~Segoufin,
``The complexity of XPath query evaluation
and XML typing'',
In Journal of the ACM 52(2):284-335, 2005.
[7] W.~Martens, F.~Neven,
``On the complexity of typechecking
top-down XML transformations'',
In Th. Computer Sc., 336(1): 153-180, 2005.
[8] F.~Neven, T.~Schwentick,
``Query automata over finite trees'',
In Th. Computer Science, 275(1-2):633-674, 2002.
[9] Worl Wide Web Consortium,
``XML Path Language (XPath Recommendation)'',
http://www.w3c.org/TR/xpath/
URL sujet détaillé :
:
Remarques : Co-enacdrement par :
Barbara FILA, Allocataire-Moniteur.
Un CDD rémunéré de façon forfataire est
envisageable pour la durée du stage (3 mois max.)
|
|
|
|
|
|
Thibaut BALABONSKI : SL306-44 Langages et automates de sable
|
|
|
Description
|
|
Les automates de sable [1] permettent de modéliser un grand nombre de phénomènes physiques basés sur la création, la destruction et le déplacement de particules. Plus précisément tout phénomène décrit par des règles locales peut être simulé par un automate de sable : seul le voisinage proche de la particule considérée est pris en compte pour déterminer son avenir, de manière similaire à ce qui est fait pour les automates cellulaires [2].
La définition des automates de sable est basée sur l'existence d'un nombre infini d'états. Cet ensemble infini (N ou Z) représente alors un alphabet. Ce stage s'intéressera aux langages définis sur cet alphabet infini, reconnus par les automates de sable.
Après s'être familiarisé avec le fonctionnement des automates de sable, on essaiera de définir les langages sur alphabet infini de manière appropriée.
Ensuite, il faudra étudier l'effet des différents modes de reconnaissance pour ces langages, en tenant compte des contraintes imposées par les automates : on ne reconnaîtra pas les mêmes langages, et pas à la même vitesse, selon le mode utilisé.
Ces différences pourront servir à séparer les langages reconnus en plusieurs classes selon des critères à définir.
Nous espérons que ce nouveau point de vue permettra d'éclaircir le comportement complexe et mal connu de ces automates.
------------------------------------
[1] J. Cervelle et E. Formenti. On sand automata. STACS 2003: 20th Annual Symposium on Theoretical Aspects of Computer Science, volume 2607 de Lecture Notes in Computer Science, pages 642−653, Springer-Verlag, 2003.
[2] P. Kurka. Topological and symbolic dynamics. Vol. 11 de Undergraduate texts, Société Mathématique de France, Paris, 2003.
URL sujet détaillé :
:
Remarques : Co-encadré par Benoît Masson (bmasson [at] i3s.unice.fr)
|
|
|
|
|
|
Denis KUPERBERG : SL306-45 Piles de sable en mode parallèle
|
|
|
Description
|
|
Les modèles les plus répandus de tas de sable (SPM [1], IPM [2]) permettent de simuler la formation d'un tas de sable de manière basique. Ils font tomber (et glisser pour IPM) des grains de sable de gauche à droite lorsque la pente est suffisante.
Une fois le modèle initial décrit, il existe deux façons de le faire évoluer. De manière séquentielle (ou asynchrone) : on déplace un seul grain à la fois. Il se pose alors le problème de choisir quel grain déplacer en premier. De manière parallèle (ou synchrone) : tous les déplacements sont opérés simultanément. On obtient un comportement plus réaliste, simulable par automates de sable [3].
Le mode séquentiel a été mieux étudié car il a des propriétés qui en facilitent l'étude. Bien qu'il soit plus naturel, pour le mode parallèle on n'a que des résultats partiels.
L'objectif de ce stage sera d'essayer d'identifier ce qui différencie les deux modes de fonctionnement, en permettant ainsi de préciser les résultats du mode parallèle. Il sera alors possible de les utiliser pour simuler de manière plus fidèle les phénomènes naturels.
On pourra ensuite envisager de créer de nouveaux modèles, multi-directionnels et multi-dimensionnels, plus généraux que SPM et IPM.
------------------------------------
[1] E. Goles et M. A. Kiwi. Games on line graphs and sand piles. Theoretical Computer Science, 115(2):321−349, 1993.
[2] E. Goles, M. Morvan, et H. D. Phan. Sand piles and order structure of integer partitions. Discrete Applied Mathematics, 117:51−64, 2002.
[3] J. Cervelle et E. Formenti. On sand automata. STACS 2003: 20th Annual Symposium on Theoretical Aspects of Computer Science, volume 2607 de Lecture Notes in Computer Science, pages 642−653, Springer-Verlag, 2003.
URL sujet détaillé :
:
Remarques : Co-encadré par Benoît Masson (bmasson [at] i3s.unice.fr)
|
|
|
|
|
|
SL306-46 Reconstruction 3D, Convection et preuve d'algorithme
|
|
|
Description
|
|
La géométrie algorithmique s'intéresse au développement d'algorithmes permettant de manipuler des objets géométriques en s'assujetissant à une arithmétique discrète. Le diagramme de Voronoï et la triangulation de Delaunay sont des constructions géométriques classiquement utilisées en Géométrie Algorithmique pour mesurer les relations de proximité entre des points. Les propriétés de ces constructions géométriques ont permis le développement d'algorithmes répondant au problème de la reconstruction 3D : A partir d'un ensemble de points échantillonnés à la surface d'un objet, ces algorithmes fournissent une approximation linéraire par morceaux de cette surface.
Outre le développement de ces algorithmes, la Géométrie Algorithmique s'intéresse au développement de preuves concernant la validité de leurs résultats. Sous certaines conditions d'échantillonnage, un certain nombre d'algorithmes (Crust, Cocone, reconstruction utilisant les voisins naturels,...) offrent des garanties géométriques et topologique sur la surface reconstruite.
Nous proposons de nous intéresser au développement d'une preuve de la validité de l'algorithme dit de Convection [1] en s'appuyant sur les résultats et les conditions d'échantillonnages présentés dans des articles récents [2,3].
L'étude de cette preuve pourra déboucher sur la production d'améliorations de l'algorithme de Convection, lorsque l'on s'éloigne des conditions optimales (échantillonnage insuffisant ou bruité).
1. R. Chaine, A geometric Convection approach of 3D reconstruction , SGP2003
2. F. Chazal, A. Lieutier, Topology guaranteeing manifold reconstruction using distance function to noisy data, to appear in proc. SoCG'06
3. F. Chazal, D. Cohen-Steiner, A. Lieutier, A Sampling Theory for Compacts in Euclidean Spaces, to appear in proc. SoCG'06.
URL sujet détaillé :
:
Remarques : Ce sujet sera coencadré par Frédéric Chazal de l'institut Mathématiques de Bourgogne
http://math.u-bourgogne.fr/topologie/chazal/
|
|
|
|
|
|
SL306-47 Etude des propriétés mathématiques de l'arithmétique des cartes graphiques
|
|
|
Description
|
|
Résumé :
L'objectif de ce stage est d'implémenter des algorithmes sur des cartes graphiques pour découvrir les caractéristiques arithmétiques des processeurs présents sur les cartes graphiques.
Description détaillée :
Les processeurs graphiques ou GPU (Nvidia GeForce, ATI Radeon, ...) sont des processeurs très puissants : entre 10 et 50 fois la puissance de calcul d'un Pentium 4. Les courbes actuelles montrent que cette tendance n'est pas prête de s'inverser, mais devrait même s'accélérer. Par exemple, le 'cell processor' que l'on retrouvera dans la future PlayStation 3 et les serveurs de calcul d'IBM est annoncé avec des performances de calcul flottant entre 50 et 100 fois celle d'un Pentium IV.
Les GPU actuels sont bien adaptés à l'exécution d'application hautement parallèle. Le nombre croissant d'application (cryptographie, base de donnée, ...) modifiée pour supporter le GPU comme coprocesseur numérique démontre l'intérêt grandissant de nombreux chercheurs pour le GPGPU [1]. Cependant l'énorme potentiel de calcul des GPU n'est que faiblement utilisé par les applications numériques actuelles. Une des raisons est le manque de communication de la part des fabricants (ATI et Nvidia) sur le détails des nombreux opérateurs arithmétiques embarqués tels que l'additionneur, le multiplieur, les évaluateurs des fonctions complexes, .... Or ces informations sont essentielles pour les chercheurs souhaitant développer des programmes efficaces et précis.
Il existe 2 grandes bibliothèques de test des opérateurs flottants pour le processeur principal (Pentium, Athlon, PowerPC,...) : paranoia et ucbtest. Ces bibliothèques donnent un certains nombre d'informations sur ces opérateurs en détectant les propriétés mathématiques vérifiées par ces derniers. Si paranoia a été porté sur GPU [2], la seconde ne l'est pas encore.
L'objectif de ce stage est d'adapter des techniques présentes dans ucbtest pour mieux comprendre comment fonctionne l'arithmétique des cartes graphiques.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL306-48 Logiques de séparation et pointeurs
|
|
|
Description
|
|
Un certain nombre de logiques, dites de séparation ou aussi spatiales, ont été récemment proposées par exemple pour raisonner localement sur des structures de données dynamiques ou pour analyser la concurrence et la mobilité dans des calculs.
Dans ce contexte on considère la logique BI (Bunched Implications Logic) ainsi que la logique des pointeurs associée PL, ce en vue de raisonner sur des programmes manipulant des pointeurs.
Le but de ce stage est d'étudier la logique PL du point de vue de la construction de preuves et de contre-modèles.
Les différentes étapes de ce travail sont :
- l'étude et l'implantation d'une méthode de preuve avec labels et contraintes pour PL, incluant la génération de contre-modèles.
- l'étude de l'extension possible de ces travaux à d'autres logiques de séparation (par exemple pour les arbres ou les graphes).
Description plus détaillée :
http://www.loria.fr/~galmiche/=stages/Suj1-L3-ENSLyon.ps
URL sujet détaillé : http://www.loria.fr/~galmiche/=stages/Suj1-L3-ENSLyon.ps
Remarques :
|
|
|
|
|
|
SL306-49 Ressources, labels et connexions
|
|
|
Description
|
|
Dans le cadre de la modélisation et du raisonnement sur des structures ou des programmes, des travaux récents ont mis en évidence la nécessité de logiques particulières dites de séparation ou spatiales.
Dans ce contexte, on étudie ici la logique BI (Logic of Bunched Implications) pour laquelle on a déjà proposé une méthode des tableaux qui construit des preuves ou des contre-modèles.
Le but de ce stage est donc d'étudier la caractérisation de la prouvabilité en logique BI du point de vue des connexions avec labels et contraintes et sa spécialisation pour les fragments IL et MILL.
Les différentes étapes de ce travail sont :
- l'étude de la caractérisation de la prouvabilité, via des connexions et des réseaux de preuve, dans BI et MILL avec des labels et contraintes, tant du point de vue théorique qu'algorithmique.
- l'implantation de la méthode associée en abordant les points suivants : génération de labels et de contraintes, résolution de contraintes et génération de contre-modèles.
Description plus détaillée :
http://www.loria.fr/~galmiche/=stages/Suj2-L3-ENSLyon.ps
URL sujet détaillé : http://www.loria.fr/~galmiche/=stages/Suj2-L3-ENSLyon.ps
Remarques :
|
|
|
|
|
|
Sylvain DUCTOR : SL306-50 Réseaux sociaux, projection de graphes et apprentissage de similarités
|
|
|
Description
|
|
Un ensemble de relations (graphes de co-auteurs, de co-citations) étant donné, l'objectif est
1/ de fournir une représentation visuelle (2D) des experts, qui préserve une similarité induite par le graphe (algorithme Isomap);
2/ de prendre en compte le retour d'un expert (je devrais être plus prêt de Mr X que de Mr Y), pour modifier la similarité considérée.
Il s'agit ainsi d'apprentissage (paramétrique ou non paramétrique) de similarité.
Le contexte d'application est celui du réseau social donné par le réseau d'excellence PASCAL (Pattern Analysis, Statistical Modelling and Computational Learning, http://www.pascal-network.org).
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL306-51 Etude du protocole Secure
|
|
|
Description
|
|
Un des problèmes clef de la sécurité des réseaux est de pouvoir s'authentifier auprès d'un serveur pour utiliser des ressources distantes. Plusieurs approches existent comme la base des mots de passe d'unix, les OTP de Lamport, ou de nouveaux protocoles qui se multiplient année après année.
Nous proposons ici d'étudier le protocole SRP inventé à l'université de Stanford et de comprendre son évolution au fur et à mesure des versions. Selon le temps, le stagiaire pourra aussi s'intéresser soit à de récentes améliorations de ce protocole (comme l'utilisation de cryptographie basée sur des courbes elliptiques), soit à des aspects plus pratiques pour accéder à des services authentifiés (smtp, imap,...).
Références :
- http://srp.stanford.edu/
- D. Stinson. Cryptographie, théorie et pratique. International Thomson Publishing, 1995.
- B. Martin. Codage, cryptologie et applications. Presses Polytechniques et Universitaires Romandes, 2004.
URL sujet détaillé :
:
Remarques : Pas de possibilité de rénumération.
|
|
|
|
|
|
SL306-52 Exploitation d'un algorithme de localisation de symboles par alignement pour la reconnaissance et la modélisation.
|
|
|
Description
|
|
Dans le domaine de l'analyse automatique de documents, l'une des préoccupations principales est de reconnaître des symboles ou des objets graphiques. Toutes les approches de reconnaissance d'images se basent soit sur une métrique entre descripteurs multidimensionnels, soit sur la minimisation d'une fonctionnelle. Dans les deux cas, il y a besoin d'un modèle ou d'une référence par rapport à laquelle on mesure ou par rapport à laquelle on construit la fonctionnelle.
Nous nous plaçons dans le contexte de l'algorithme de reconnaissance existant et fourni qui cherche à aligner des groupes de primitives graphiques par calcul de transformation affine. Il n'a jamais été testé ou mis en oeuvre dans un contexte où l'on n'a aucune connaissance a priori du modèle à reconnaître ou rechercher. Nous proposons donc de mettre en oeuvre une méthode permettant de partir d'exemples sélectionnés à la volée par un utilisateur, en d'en construire un modèle à l'aide de l'algorithme cité. L'approche devra notamment être testée dans un contexte de symboles fortement noyés et connectés dans un environnement graphique complexe.
URL sujet détaillé : http://www.mines.inpl-nancy.fr/~lamiroy/sujet_ens_2006.pdf
Remarques :
|
|
|
|
|
|
Jeremy PLANUL : SL306-53 Customisation du processeur Xtensa pour le calcul par intervalles
|
|
|
Description
|
|
Contexte
La société Tensilica fournit actuellement une des méthodologies les plus performantes pour la conception de systèmes sur puce, avec des outils de CAO permettant de manière automatique de spécialiser (customization) les instructions du processeur RISC 32 bits qui est le coeur du système. Ainsi grâce à un langage haut niveau, sans recours à VHDL ou Verilog, il est possible d\'ajouter non seulement de nouvelles unités de calcul généralistes (de type UAL ou unité de calcul flottante) mais aussi des unités spécialisées ou dédiées (par exemple pour la cryptographie, la recherche de séquences génomiques, ...).
Objectif
L\'arithmétique des intervalles est l\'une des techniques pour évaluer l\'impact des erreurs d\'arrondi en calcul scientifique et pour faire du calcul \"sans erreur\". Ainsi une valeur réelle sera remplacée par un intervalle, encadrant la valeur.
Le calcul par intervalle est très utilisé pour garantir des calculs fiables dans les systèmes embarqués tels les robots autonomes. Ces robots naviguent grâce à des systèmes de localisation basés sur des calculs itératifs. Une dérive des calculs pouvant avoir des effets catastrophiques pour ces robots, les algorithmes implantés sur les robots ont donc recours au calcul par intervalle pour estimer la précision des calculs au cours du temps.
L\'arithmétique des intervalles est l\'une des techniques pour évaluer l\'impact des erreurs d\'arrondi en calcul scientifique. La définition des opérations de base pour deux intervalles [a,b] et [c,d] qui sont des sous ensembles des réels (-infini, +infini),
[a,b] + [c,d] = [a+c, b+d]
[a,b] - [c,d] = [a-d, b-c]
[a,b] * [c,d] = [min (ac, ad, bc, bd), max (ac, ad, bc, bd)]
[a,b] / [c,d] = [min (a/c, a/d, b/c, b/d), max (a/c, a/d, b/c, b/d)]
Le principal problème de ce type de calcul est que les arrondis sont fait par défaut pour calculer la borne inférieure, et par excès pour calculer la borne supérieure. Ce changement de calcul d\'arrondi est très pénalisant pour un processeur classique car il nécessite un changement très coûteux du mode d'arrondi.
Travail à réaliser
Le but de ce stage est donc d\'implanter les opérateurs arithmétiques classiques pour le calcul par intervalle, en intégrant une double gestion d\'arrondi.
En partant de la version de référence du processeur RISC Tensilica, on étudiera les performances des opérations de base et on spécifiera des instructions spécialisées permettant d\'accélérer les calculs (versions scalaires et versions SIMD).
L\'impact des optimisations sera évaluée sur des benchmarks significatifs utilisant l\'arithmétique des intervalles.
Matériel à disposition
Station de travail équipée des outils de CAO de Tensilica
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Thomas BRAIBAN : SL306-54 Définition et implémentation d'une machine abstraite.
|
|
|
Description
|
|
Nous travaillons sur la définition d'une algèbre de processus pour la
modélisation de la programmation distribuée. Les travaux menés
jusqu'ici ont débouché sur la définition d'un premier calcul (appelé
Georges), dont il s'agit de comprendre l'expressivité et l'adéquation
vis-à-vis des phénomènes que l'on veut modéliser.
Ce calcul appartient à la famille des modèles tels que le pi-calcul ou
join, qui permettent de représenter diverses formes d'interaction au
sein de systèmes concurrents. Ce coeur `standard' est enrichi par
l'ajout de constructions servant à décrire la structuration des
calculs, et en particulier les phénomènes liés à la distribution et au
partage de sous-calculs -- idées que l'on trouve souvent exprimées à
travers la notion de composant. Ainsi, les calculs ne se déroulent pas
uniquement au sein d'un composant, mais peuvent aussi faire intervenir
une modification de la structure même du système.
À l'heure actuelle, le calcul tel qu'il est défini est muni d'un
système de types visant à garantir l'exclusion d'un certain nombre
d'erreurs lors de l'exécution des programmes, erreurs liées à la
gestion de la portée des identificateurs. L'étape successive est
d'évaluer le caractère `réaliste' du calcul, en essayant de comprendre
d'une part s'il permet de représenter les phénomènes que l'on cherche
à modéliser, et d'autre part s'il peut servir de point de départ pour
la définition d'un langage de programmation, et en particulier s'il
est possible d'implémenter ce calcul de manière raisonnable. Pour
s'intéresser à ce deuxième aspect, on souhaite définir une machine
abstraite pour l'exécution des processus décrits dans ce modèle.
Le déroulement du stage devrait être le suivant:
- Familiarisation avec le calcul tel qu'il a été proposé, et avec les
choix de conceptions qui ont été faits lors de sa définition.
- Définition (sur papier) de la machine abstraite, de manière
formelle. Cette définition doit en quelque sorte être un raffinement
du calcul de départ, prenant en question des questions liées à
l'exécution des processus. Lors de la définition de la machine
abstraite, il faut d'une part pouvoir établir la correspondance avec
le calcul originel. D'autre part, la machine doit en même temps être
suffisamment précise pour que chaque pas de calcul dans la machine
soit implémentable de manière directe (en général, un pas de calcul
dans le calcul originel correspondra à plusieurs pas de la machine).
- Implantation de tout ou partie de la machine abstraite, afin de
pouvoir se livrer à quelques expériences.
- Si le temps le permet, ébauche de la preuve de correction de la
machine abstraite. Cette étape, qui est bien entendu indispensable
pour justifier le fait que la machine fait bien ce pour quoi elle a
été conçue, représente un très gros travail. L'idée de ce stage est
plutôt de faire des expériences autour de la définition de la
machine (en gardant bien entendu en tête la correction d'ycelle),
mais, vue la durée du stage, il semble illusoire d'aboutir à une
preuve complète accompagnée d'une implémentation.
Références: le calcul sur lequel nous travaillons étant encore en
gestation, le plus simple est probablement de contacter
D. Hirschkoff, D. Pous ou T. Hirschowitz pour toute précision sur le
sujet du stage.
URL sujet détaillé :
:
Remarques : Le stage sera co-encadré par monsieur Damien Pous, doctorant au LIP.
|
|
|
|
|
|
Martin DELACOURT : SL306-55 Automates cellulaires
|
|
|
Description
|
|
Les automates cellulaires sont un modèle de calcul très simple qui permet de modéliser un calcul massivement parallèle.
L'objectif de ce stage est d'explorer l'impact qu'a le choix du voisinage (le voisinage décrit le graphe d'interaction des cellules, c'est-à-dire comment l'information et le calcul peuvent se propager) sur la puissance des automates cellulaires en termes de reconnaissance de langages en dimension 2 (donc des langages d'images).
Deux voisinages ont été principalement étudiés en dimension 2 : le voisinage de Von Neuman (4 voisins et la cellule elle-même) et celui de Moore (8 voisins et la cellule), et l'on sait qu'ils ont des propriétés assez différentes. On connaît par exemple un résultat d'accélération de la reconnaissance d'un langage par une constante dans le cas du voisinage de Moore, tandis qu'un tel résultat n'est pas connu pour le voisinage de Von Neumann.
On s'intéressera principalement à la plus petite classe de complexité : les langages reconnus en temps-réel, c'est-à-dire le plus petit temps nécessaire pour que toute l'information de l'image ait pu atteindre l'origine (où a lieu la reconnaissance). Le choix du voisinage a un impact très fort sur cette classe (il détermine la valeur de ce "temps minimal") et l'on cherchera à caractériser les voisinages pour lesquels cette classe est la même, les conditions pour qu'un voisinage reconnaisse plus de langages qu'un autre en temps réel, etc.
Il y a de nombreuses questions et de nombreuses pistes à suivre...
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL306-56 Exploration d'espaces de pavages tridimensionnels
|
|
|
Description
|
|
Les espaces de pavages (graphes dont les sommets sont les pavages d'une figure donnée, et où deux pavages sont liés par une arête si l''on peut passer de l'un à l'autre par une transformation locale appelée ''flip'') sont très intriguants, et leur structure est si peu connue que leur connexité n'est pas prouvée pour des cas simples. Ils jouent pourtant un rôle primordial dans la modélisation physique (cristallographie).
Nous nous intéressons en particulier aux pavages tridimensionnels, avec des parallépipèdes construits sur un nombre fini de vecteurs. Nous avons récememrnt introduit une méthode, purement combinatoire, de représentation de tels pavages, qui a conduit, entre autres aux resultats suivants :
Avec 5 vecteurs, il n'y a qu'une position relative des vecteurs, et l'on a déjà obtenu des résultats de connexité, et d'autres résultats structurels en orientant ''canoniquement'' les arêtes de l'espace des pavages. Avec 6 vecteurs, il y a quatre positions relatives des vecteurs. Pour trois cas, la connexité est avérée, le problème de la connexité est ouvert dans le dernier cas.
L'objet du stage consiste à tester quelques conjectures (avec 5 ou 6 vecteurs), soit pour les infirmer par un contrexemple, soit pour les affiner et cerner exactement les dififcultés. Cela suppose la progression suivante :
a) lecture et discussion à partir d'articles de référence
b) implementation d'un outil de tests
c) expérimentation
d) analyse des résultats, rédaction du rapport.
URL sujet détaillé :
:
Remarques : bibliographie principale :
Aspects combinatoires des pavages.
Frédéric Chavanon
Thèse LIP 2004-06
(http://www.ens-lyon.fr/LIP/Pub/PhD2004.php)
|
|
|
|
|
|
SL306-57 Alignement de pages manuscrites sur leurs transcriptions
|
|
|
Description
|
|
Les images de documents manuscrits anciens, actuellement numérisés en masse pour des raisons de préservation et d'accessibilité, sont couramment utilisées par les philologues qui s'intéressent notamment aux problèmes de datation et d'édition de textes. Ainsi, afin de permettre une utilisation plus aisée de cette masse de documents, il est nécessaire de recourir à une indexation automatique qui représente des enjeux importants tant du point de vue scientifique, que des aspects applicatifs. L'indexation a en effet pour objectif de permettre un accès rapide et facile à des passages spécifiques dans un document, c'est à dire, à l'image où à la partie de l'image correspondant à un texte (une phrase, un paragraphe) spécifique. Or, les techniques d'OCR (reconnaissance automatique des caractères) qui constituent une étape préalable à l'indexation, ne peuvent être exploitées sur les documents manuscrits anciens, du fait de leur mauvais état de conservation et de l'irrégularité trop importante de l'écriture.
Pour une grande partie de ces oeuvres nous disposons aujourd'hui des transcriptions rédigées manuellement. Toutefois, ces transcriptions, bien que complètes, ne permettent pas l'indexation des documents. En effet, l'absence de liaisons entre les parties de la description textuelle et leur partie image correspondante rend impossible l'accès rapide aux documents manuscrits.
Dans ce contexte, l'objectif de ce stage consiste à développer un processus automatique d'alignement. Il s'agit de trouver automatiquement, pour une partie de la transcription textuelle (quelques mots), l'endroit précis correspondant dans l'image du document manuscrit. Cette problématique est étroitement liée à la thématique de reconnaissance de mots dans les images de documents. Ainsi, reformulant le problème, pour un ensemble d'imagettes correspondant à un ensemble de mots, l'objectif consiste à en déterminer la description textuelle. Cependant, l'espace des solutions est restreint par le texte de la transcription.
Contrairement à la reconnaissance traditionnelle, dans ce contexte la correspondance imagette - texte n'est donc pas pris au niveau du caractère ou au niveau du mot, mais au niveau de séquence de mots. Cette démarche bénéficie d'un avantage considérable qui est l'utilisation de l'information associée à la succession des mots. Pour cette raison, l'approche proposée dans le cadre de ce stage devra se baser sur un mode de fonctionnement favorisant l'exploitation de cette information. A titre d'exemple nous pouvons citer les algorithmes permettant de faire un alignement de chaînes de symboles basés sur la programmation dynamique [2]. Toutefois, la nature du problème nécessite une adaptation de ces algorithmes au traitement des chaînes de caractéristiques.
Méthode:
Le travail de ce stage consistera donc dans un premier temps à réaliser une étude bibliographique brève concernant les approches d'alignement de documents manuscrits, mais également d'alignement des génomes, puisque les problématiques dans ce domaine de la bioinformatique s'avèrent être très similaires. Dans un second temps, une solution au problème de l'alignement de documents manuscrits devra être élaborée. Une approche envisageable consiste à réaliser une segmentation de l'image de manière à isoler les mots manuscrits (dans le cadre de ce stage, cette partie sera éffectuée manuellement). Des descripteurs devront ensuite être définis afin de constituer des chaînes de caractéristiques représentant des ensembles de mots, extraits d'une part à partir de l'image, et d'autre part à partir de la transcription. Une distance devra alors être élaborée, compatible avec le formalisme de la programmation dynamique de manière à permettre une certaine tolérance due aux erreurs éventuelles de segmentation et de transcription. L'information de cette distance permettra de déterminer la correspondance la plus probable entre un ensemble de mots issu de la transcription et ce même ensemble de mots dans une image de document manuscrit.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Xavier PUJOL : SL306-58 Évaluation de fonctions élémentaires en virgule flottante sur FPGA
|
|
|
Description
|
|
Ce stage s'inscrit dans le cadre du développement de la bibliothèque d'opérateurs matériels FPLibrary [1]. Cette bibliothèque offre toute une gamme d'opérateurs arithmétiques classiques (addition, soustraction, multiplication, division et racine carrée) décrits en VHDL et destinés à être utilisés sur FPGA. Ces opérateurs supportent deux formats de représentations des nombres réels (virgule flottante et système logarithmique), ainsi qu'une précision arbitraire, pour permettre à un utilisateur de cette bibliothèque de choisir la solution qui convient le mieux à son application. Malheureusement, les opérateurs de FPLibrary, du fait qu'ils tournent sur un FPGA cadencé à 100 MHz, sont par conséquent plus de 20 fois plus lents que les opérateurs correspondants sur un Pentium Xeon cadencé à 2,4 GHz.
Par contre, FPLibrary peut concurrencer les processeurs classiques sur le terrain des fonctions élémentaires (telles que logarithme, exponentielle, sinus, arc-tangente, etc...). En effet, contrairement à ce que l'on pourrait croire, les processeurs actuels ne disposent pas d'unités spécialisées dans le calcul de telles fonctions. Celles-ci sont généralement calculées en logiciel (grâce à une libm) ou micro-codées dans le processeur (celui-ci remplace l'instruction assembleur correspondante par une suite d'instructions permettant d'évaluer effectivement la fonction en utilisant les additionneurs et multiplieurs flottants dont il dispose).
L'intérêt d'aborder ce problème sur FPGA est que nous sommes libres de développer un algorithme beaucoup mieux adapté et plus finement optimisé, en tirant parti du parallélisme inhérent à la structure du FPGA et du vaste champ d'exploration matériel qu'il nous offre. Nous avons ainsi réalisé des opérateurs pour le logarithme et l'exponentielle, et ceux-ci se révélèrent jusqu'à 10 fois plus rapides que leurs équivalents sur un Pentium Xeon à 2,4 GHz en simple précision [2]. Nous sommes actuellement en train de développer de manière similaire un opérateur pour calculer sinus et cosinus.
Nous proposons d'aborder la suite de deux manières différentes :
- soit continuer sur cette piste, et développer des opérateurs pour d'autres fonctions élémentaires ;
- soit trouver de nouveaux algorithmes pour permettre d'évaluer les fonctions existantes (log, exp, sin, cos) en double précision, car les opérateurs actuels ne gèrent que jusqu'à la simple précision.
Ces deux axes de recherche peuvent bien entendu être répartis sur deux stages distincts.
[1] Jérémie Detrey and Florent de Dinechin.
Outils pour une Comparaison sans A Priori entre Arithmétique Logarithmique et Arithmétique Flottante.
In M. Auguin and D. Lavenier, editors, Architecture des Ordinateurs,
volume 24(6) of Technique et Science Informatiques, pages 625-643. Lavoisier, France, November 2005.
http://perso.ens-lyon.fr/jeremie.detrey/publications/pub/DetDin2005_tsi.pdf
[2] Jérémie Detrey and Florent de Dinechin.
Parameterized Floating-Point Logarithm and Exponential Functions for FPGAs.
LIP research report 2006-02, January 2006.
http://perso.ens-lyon.fr/jeremie.detrey/publications/pub/DetDin2006_rr-lip.pdf
URL sujet détaillé :
:
Remarques : Ce stage peut être découpé en deux si plusieurs étudiants sont intéressés.
Ce stage sera co-encadré par Florent de Dinechin.
L'étudiant sera rémunéré s'il ne dispose pas déjà d'un financement.
|
|
|
|
|
|
Cedric AUGONNET : SL306-59 Optimisation des communications sur réseaux rapides par utilisation de RDMA
|
|
|
Description
|
|
Les travaux de l'équipe Runtime dans le domaine du calcul parallèle à
hautes performances ont notamment conduit à l'élaboration d'une
interface de communication nommée Madeleine capable d'effectuer des
transferts de données rapides en s'appuyant sur différents protocoles
bas-niveau pour réseaux rapides (Myrinet, SCI, etc.) Son interface est
orientée "envoi de messages" et est fondée sur une construction
incrémentale des messages. Chaque segment de message possède ses
propres contraintes de transmission et de réception. L'originalité de
Madeleine est de permettre une sélection dynamique d'optimisations de
transmission des données en fonction de ces contraintes (exprimées par
l'application). Pour effectuer ces optimisations, la bibliothèque
Madeleine utilise différentes stratégies qui prennent en compte les
caractéristiques du réseau sous-jacent ainsi que la taille et les
constraintes de chacun des segments traités depuis le début d'un
message.
La mise en oeuvre de Madeleine sur des technologies de communications
récentes telles que Myrinet/MX a permis de mettre en évidence un
certain nombre de situations où l'utilisation des primitives
classiques (send/recv) des interfaces de communication bas-niveau
limitent le degré d'optimisation applicable aux transferts de données.
Dans ce contexte, l'objectif de ce mémoire est de mener une étude
portant sur l'utilisation de mécanismes d'écriture à distance (RDMA),
disponibles sur de nombreuses technologies réseaux contemporaines, au
sein de la bibliothèque Madeleine. Il s'agira de mettre en évidence
les extensions nécessaires au niveau des différents modules de la
bibliothèque (notamment l'optimiseur) et d'évaluer les gains qui
pourront en résulter à l'aide d'un prototype développé au-dessus de
MX/Myrinet.
URL sujet détaillé :
:
Remarques : Stage co-encadré avec Elisabeth Brunet (Elisabeth.Brunet.fr)
|
|
|
|
|
|
SL306-60 Opérateurs arithmétiques pour la cryptographie basée sur les courbes elliptiques
|
|
|
Description
|
|
1. Contexte.
La cryptographie est la branche de la théorie de l'information qui se préoccupe de la confidentialité des échanges d'informations. La cryptographie à clef publique, apparue dans les années 70 avec le cryptosystème RSA, permet d'effectuer des signatures électroniques, des authentifications, d'échanger des clefs de chiffrement etc. Elle est devenue incontournable de nos jour.
La cryptographie à clef publique basée sur les courbes elliptiques est maintenant très largement utilisée. Elle garantie une plus haute sécurité que RSA, tout en étant plus efficace. Cette efficacité est liée en grande partie aux opérations d'addition et de multiplication dans un corps fini.
2. Objectif du stage.
Ce stage consistera à implanter en C un nouvel algorithme pour multiplier, additionner dans un corps fini, ainsi que les opérations classiques sur les courbes elliptiques. L'objectif étant de comparer les performances de ce nouvel algorithme par rapport au méthodes usuelles.
URL sujet détaillé : http://gala.univ-perp.fr/~cnegre/sujet-stage-cnegre.pdf
Remarques :
|
|
|
|
|
|
Francois DUPRESSOIR : SL306-61 Exploitation de la construction syntaxique des verbes pour l'évaluation automatique de l'influence sémantique de leurs compléments.
|
|
|
Description
|
|
De nombreux verbes changent de sens selon le type de complément qui suit, mais aussi selon sa présence ou son absence.
Par exemple dans la phrase "Il vient du nord.", le complément "du nord", et plus particulièrement la préposition "de", détermine un sens particulier de venir (définition C dans le TLFi [1]). Si ce complément est absent, le sens de "venir" est différent. Ce complément a donc un rôle important dans la phrase.
Le but de ce stage est d'élaborer un ensemble d'algorithmes permettant de déterminer l'importance des compléments de verbes selon la construction syntaxique des verbes associés.
Cette tâche est destinée à être utilisée dans un processus de compression de phrases [2].
En effet, selon l'importance des compléments, ils pourront être supprimés ou conservés dans les phrases.
Pour la mise en oeuvre, le stagiaire dispose du système opérationnel SYGMART [3] qui permet de manipuler des structures de données de type arbre, et de SYGFRAN, programmé un SYGMART, qui permet d'effectuer une analyse morpho-syntaxique sur des phrases en français en produisant, à partir d'un texte brut, leur arbre syntaxique.
La réalisation de ce stage pourra nécessiter la création d'une ressource lexicale sur les différentes constructions syntaxiques des verbes utilisés dans les expérimentations.
[1] http://atilf.atilf.fr
[2] Yousfi-Monod M., Prince V., /Utilisation de la structure morpho-syntaxique des phrases dans le résumé automatique/, à TALN 2005 , Dourdan, Juin 2005, pp. 193-202.
[3] Jacques Chauché. Un outil multidimensionnel de l'analyse du discours. In Coling-84, pages
11-15, Standford University, California, 1984, http://www.lirmm.fr/~chauche/ExempleAnl.html
URL sujet détaillé :
:
Remarques : Co-encadrant: Augusta Mela, maître de conférences en sciences du langage, spécialiste de TAL
Note : sujet déjà pris
|
|
|
|
|
|
Vincent NIVOLIERS : SL306-62 Partitions spaciale soumises à contraintes
|
|
|
Description
|
|
Le principe est de définir une méthode construisant des partitions spatiales soumises à des contraintes différentes selon l'utilisation du modèle partitionné : lancer de rayons logiciel, lancer de rayons openGL, affichage de maillages par strips, ou affichage avec limitation de l'overdraw.
L'objectif est de proposer une méthode générale utilisable dans les différents cas et de déterminer des heuristiques de construction adaptées à chaque utilisation.
1. Partitions spatiales (utilisees par plusieurs algorithmes) :
** le lancer de rayons, les méthodes adaptées à ce cas :
"heuristic ray shooting algorithms"
http://www.cgg.cvut.cz/~havran/DISSVH/phdthesis.html
v. havran
et
"realtime ray tracing and interactive global illumination"
http://www.sci.utah.edu/~wald/PhD/
i. wald
2. Réorganisation de maillages pour limiter soit le volume de données à transmettre à la carte graphique pour afficher un objet (construction de strips), soit pour limiter l'"overdraw" (nombre de fois où un pixel est dessiné). Ces deux méthodes sont décrites dans :
"Optimization of Mesh Locality for Transparent Vertex Caching"
http://research.microsoft.com/%7Ehoppe/tvc.pdf
h. hoppe
et
"Triangle Order Optimization for Graphics Harwdare Computation Culling"
http://www.pedrosander.com/docs/too.pdf
p. sanders
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|