|
SL307-1 Algorithme de simplification optimale d'axe médian pour l'analyse d'objets 3D
|
|
|
Description
|
|
Introduction
============
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.
L'axe médian n'est cependant pas minimal : sur l'image ci-dessous,
deux représentations du cube discret par des boules sont possibles.
Cependant, on se rend compte la représentation de droite est plus
efficace dans le sens où elle contient moins de boules.
D'un point de vue algorithmique, même s'il existe de nombreux
algorithmes permettant d'approcher cet axe médian minimal en nombre de
boules, l'extraction de cet axe médian est un problème NP-complet
(très difficile).
L'objectif du stage est de proposé un algorithme de calcul de l'axe
médian minimal par une approche exhaustive (ou approche
complète). La théorie nous dit qu'un tel algorithme pourra se
dérouler en temps exponentiel mais avec des stratégies de codage
adaptées, nous souhaitons obtenir un algorithme raisonnable en
temps.
Le ou les étudiants commenceront par s'approprier le code existant
et devront proposer une implémentations efficace de l'algorithme de
simplification exhaustif.
URL sujet détaillé : http://liris.cnrs.fr/~dcoeurjo/stages/2006_TER_simplification_axe_median.html
Remarques :
|
|
|
|
|
|
SL307-2 Algorithme de reconnaissance de plans 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.
Afin de décrire la géométrie de ces objets, les plans discrets, analogues discrets des plans euclidiens ont été définis. Ils permettent de caractériser de manière analytique des ensembles de voxels coplanaires.
Etant donné un ensemble de voxels, le problème de la reconnaissance de plan est de décider si cet ensemble de voxels est un morceau de plan discret, et si oui, de calculer les paramètres de ce plan. Plus exactement, pour un ensemble de voxels donné, nous serons intéressés par le calcul des paramètres de l'ensemble des plans euclidiens dont la discrétisation contient l'ensemble de voxels initial.
La méthode proposée est basée sur une réécriture du problème dans un espace dual 3D où chaque plan euclidien est représenté par un point (les coordonnées de ce point sont fonction des paramètres du plan). Ainsi, pour un ensemble de voxels coplanaires donné, l'ensemble des plans recherché est représenté par un polyèdre (appelé préimage) dans l'espace dual. Le but de ce stage est de coder un algorithme efficace de reconnaissance de plan discret avec calcul de la préimage.
URL sujet détaillé : http://liris.cnrs.fr/isabelle.sivignon/algo_reco_plans.html
Remarques : Co-encadrement avec Isabelle Sivignon.
|
|
|
|
|
|
Mathilde NOUAL : SL307-3 Les jeux CP
|
|
|
Description
|
|
Les jeux CP sont une nouvelle présentation et surtout une
généralisation des jeux stratégiques dans lesquels on étend les
notions habituelles pour obtenir des résultats nouveaux et plus
généraux.
Le but du stage est d'explorer diverses structures de jeux et d'examiner
l'avantage qu'il y aurait à les considérer du point de vue des jeux
CP.
Le prérequis sont une formation en mathématique discrète comme celle
délivrée en licence d'informatique fondamentale de l'ENS de Lyon et
un tutoriel que j'ai écrit.
N.B.: C provient de Conversion et P de Préférence, qui sont les deux
concepts de base des jeux CP.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-4 Capture des mouvements fins du visage en utilisant l'information d'éclairement (Shape From Shading)
|
|
|
Description
|
|
MOTIVATIONS
La capture des mouvements d'un visage (facial motion capture) est un domaine de recherche actif depuis de nombreuses années. De bons résultats sont possibles [Wang04],
même sans avoir recours à l'utilisation de marqueurs. Ces méthodes sont basées sur la reconnaissance de points caractéristiques dans l'image. Ces points étant soit représentés par des marqueurs (pastilles) collés sur le visage, soit détectés comme le coin des yeux, des lèvres, etc. Cependant, ces méthodes ne peuvent capturer les déformations fines du visage (plissement du front, autour des yeux, des joues, etc.) à cause du nombre limité de points.
D'un autre coté, les techniques de reconstruction de formes 3D (maillage) à partir de l'image d'éclairement (Shape from Shading) ont énormément progressé ces dernières années. On commence à obtenir des résultats intéressants sur des photos de visage [Zeng05] en utilisant l'information de luminance comme information d'éclairement.
L'idée de ce stage serait d'explorer en quoi l'utilisation de l'image d'éclairement peut aider à la capture du mouvement du visage (facial motion capture), avec en particulier la capture des déformations de peaux : plissement, paupières.
OBJECTIF
Nous disposons d'une implémentation d'un algorithme de Shape from Shading [Zeng05] pouvant servir de base à ce projet.
Le stage peut alors prendre deux directions.
Direction 1 (orienté reconstruction)
Les méthodes de shape from shading [SFS, Zeng05] existantes produisent pour l'instant un résultat globalement acceptable mais loin d'être parfait (certains points doivent être entrés manuellement, les échelles de la forme reconstruite sont assez approximatives, etc.). Une partie de ces défauts sont dus à la supposition que la peau se comporte vis-à-vis de la lumière comme un matériau totalement diffus ce qui n'est que partiellement vrai. Il serait intéressant d'explorer l'utilisation d'une fonction de réflectance spécifique de la peau pour la reconstruction de visage. Nous disposons des telles données.
Direction 2 (orienté maillage)
L'algorithme de shape from shading produit une carte de hauteur pour chaque image de l'animation. Cette carte de hauteur peut facilement être triangulée pour obtenir un maillage. Cependant, ce maillage n'est pas continu dans le temps. Cette deuxième direction consistera à reconstruire au cours de l'animation un maillage unique du visage et à représenter chaque pas de l'animation comme une déformation de ce maillage. [Zhang05]
En pratique : Implémentation logiciel en C++ / OpenGL / (OpenCV)
BIBLIO
[Zeng05] Interactive Shape from Shading
Gang Zeng and Yasuyuki Matsushita and Long Quan and Heung-Yeung Shum
CVPR '05: Proceedings of the 2005 IEEE Computer Society Conference on Computer Vision and Pattern Recognition (CVPR'05) - Volume 1
[Wang04]
High Resolution Acquisition, Learning and Transfer of Dynamic 3-D Facial Expressions,
Yang Wang, Xiaolei Huang, Chan-Su Lee, Song Zhang, Zhiguo Li, Dimitris Samaras, Dimitris Metaxas, Ahmed Elgammal, Peisen Huang,
In Computer Graphics Forum (in conjuction with EuroGraphics 2004), pp. III: 677-686
[SFS] Shape from Shading: A Survey
http://www.cs.ucf.edu/~vision/papers/shah/99/ZTCS99.pdf
[Zhang05]
Image-Driven Re-targeting and Relighting of Facial Expressions,
Lei Zhang, Yang Wang, Sen Wang, Dimitris Samaras,
In Computer Graphics International 2005
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-5 Un radar pour l'internet
|
|
|
Description
|
|
Il s'agit de faire des mesures périodiques de la topologie de l'internat autour d'une source, avec des outils de type traceroute.
Il y a notamment un travail de visualisation des données obtenues, sous forme d'un radar.
Plus de détails dans le sujet en pdf.
URL sujet détaillé : http://www.liafa.jussieu.fr/~latapy/Stages/sujet_radar.pdf
Remarques : co-encadré avec Clémence Magnien
|
|
|
|
|
|
SL307-6 Compression de très grands graphes
|
|
|
Description
|
|
Il s'agit de mettre en oeuvre des techniques raffinées de compression de très grands graphes, proposées récemment dans des articles de recherche, ainsi que d'explorer quelques nouvelles directions.
Plus de détails dans le sujet en pdf.
URL sujet détaillé : http://www.liafa.jussieu.fr/~latapy/Stages/sujet_compression.pdf
Remarques : co-encadrement avec Clémence Magnien
|
|
|
|
|
|
SL307-7 Structure multi-échelle des grands graphes
|
|
|
Description
|
|
La plupart des très grands graphes rencontrés en pratique ont une structure multi-échelle : ils contiennent des zones denses peu connectées entre elles, et les zones denses ont elles-mêmes cette structure.
Il s'agit dans ce stage d'étudier les propriétés de ces structures, sur la bases de programmes les calculant qui sont fournis.
Plus de détails dans le pdf.
URL sujet détaillé : http://www.liafa.jussieu.fr/~latapy/Stages/sujet_communautes.pdf
Remarques : co-encadrement avec Clémence Magnien
|
|
|
|
|
|
Lionel RIEG : SL307-8 Coalitions optimales
|
|
|
Description
|
|
Les systèmes multi-agents sont des systèmes de transitions dont l'évolution est soumise aux actions simultanées de plusieurs agents :
à chaque étape, les agents choisissent l'action qu'ils souhaitent faire, et la transition correspondant à l'ensemble de ces choix est appliquée. La logique ATL a été définie pour spécifier des propriétés de ces systèmes : cette logique est une extension de la logique CTL permettant d'exprimer le fait qu'une coalition d'agents a (ou n'a pas) une stratégie permettant d'atteindre un objectif, quoi que fassent ses adversaires.
Nous proposons d'étudier un aspect un peu différent d'ATL : au lieu d'évaluer une formule d'ATL, le problème est maintenant de chercher une coalition optimale (c-à-d. avec le minimum d'agents) permettant d'atteindre un objectif. À notre connaissance, ce problème n'a jamais été étudié, et peut être élargi en de multiples directions (coalition optimale pour le problème d'accessibilité, extension à l'ensemble de la logique ATL, autres restrictions sur les coalitions,...)
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/l3-07-tbnm-1.html
Remarques : Co-encadrant: Thomas BRIHAYE, LSV, ENS de Cachan
|
|
|
|
|
|
SL307-9 Vers la Vérification Automatique de services Web
|
|
|
Description
|
|
Les services Web permettent par exemple de réserver un voyage en train et un hotel tout en louant une voiture ou bien de commander des films,... La question de la sécurisation et de la confidentialité des échanges est cruciale pour assurer le développement de ces services et il s'agit d'un problème théorique et pratique très important à l'heure actuelle. Des normes existent
pour ces services, qui sont décrits usuellement dans une syntaxe XML (selon la norme SOAP). L'exécution des services et leurs principes sont proches de ceux des protocoles cryptographiques (protocoles d'échanges dans un milieu non-s^ur, comme ssh) et l'objectif du stage est de réaliser les outils qui permettent de reprendre ce qui existe pour aller vers la vérification automatique des services web.
Dans un premier temps le travail consiste à écrire un traducteur de la syntaxe XML vers le langage source d' outils de vérification automatique, tels AVISPA { t http://www.avispa-project.org/} ou Trust { t http://www.lif.univ-mrs.fr/spip.php?article259/}.
Ensuite, il s'agit de s'attaquer aux problèmes de vérification de la traduction obtenue qui contient des opérateurs associatifs-commutatifs: en
effets ceux-ci apparaissent implicitement via la syntaxe XML qui décrit les objets (ici les services) sous forme d'arbres d'arité non-bornée. Un travail en cours propose une technique permettant de traiter ces opérateurs en
combinaison avec ceux du modèle classique d'attaque dit modèle de Dolev-Yao et
il s'agit de voir comment mettre en oeuvre ce résultat de manière efficace, ce
qui pose des problèmes pratiques et théoriques.
URL sujet détaillé : http://www.cmi.univ-mrs.fr/~lugiez/Recherche/Stages/stageL3-06-07.pdf
Remarques :
|
|
|
|
|
|
SL307-10 Vérification de modules Mandrake 10.1
|
|
|
Description
|
|
La version de KDE de la distribution libre mandrake 10.1 se bloque
régulièrement obligeant à rebooter la machine. L'objectif du stage est de
mettre en oeuvre les outils et techniques d'analyse de logiciels pour
déterminer les erreurs qui amènent un tel comportement. Plus que de trouver
l'erreur, l'intér^et du stage proposé est de faire le point sur les outils
qui se développent actuellement pour l'analyse des programmes, en particulier
compte tenu des récents développements réalisés pour la vérification des
programmes qui comportent des structures de données manipulant des
pointeurs. Un objectif concret sera de choisir un module susceptible de donner
lieu à une erreur et d'en faire l'analyse avec les outils existant. Cette
étude pratique peut donner lieu à un développement théorique pour proposer de
nouvelles méthodes d'analyse ou des améliorations de celles qui existent.
Prerequis Une bonne connaissance de Linux et des environnements KDE est
souhaitable.
URL sujet détaillé : http://www.cmi.univ-mrs.fr/~lugiez/Recherche/Stages/stageL3-06-07.pdf
Remarques :
|
|
|
|
|
|
SL307-11 Verification of the clock synchronization algorithm of the FlexRay protocol
|
|
|
Description
|
|
Time-triggered protocols are the basis for communication architectures in the avionics and automotive domains where software controls have largely replaced mechanical interconnections ("X-by-wire" applications). We are currently working on a framework for the formal verification of the functional correctness of the main building blocks of these protocols, such as medium access control and clock synchronization algorithms under explicit fault hypotheses. We wish to validate this framework by verifying the algorithms used in the Flexray architecure (http://www.flexray.com/).
The subject of this internship is to formalize in a theorem prover the proof of the correctness of the clock synchronization algorithm implemented in the FlexRay protocol. The correction of this algorithm involves proving many arithmetic results where many can be proven using automatic solvers. Thus, we intend to use both an interactif theorem prover (like Isabelle or Coq) and an automatic solver to carry out this formalization.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Alexandre DEROUET-JOURDAN : SL307-12 Etude d'un jeu combinatoire récent =96 le clobber.
|
|
|
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 ".
Clobber est un jeu récent introduit par Nowakowski, Albert et Grossman en 2002. Nous étudions une variante définie par Duchêne, Faria et Gravier en 2005. Des pierres de couleur noire ou blanche sont placées sur un graphe. Chaque mouvement consiste à choisir une pierre, puis une pierre voisine de couleur différente. On mange alors la pierre voisine avec la première pierre (qui prend la place de sa voisine dans le graphe). L'objectif est de finir avec le moins de pierres restantes possible. Des études ont déjà été menées sur les hypergraphes, les graphes de Hamming etc. Nous nous intéressons plus particulièrement au cas des graphes de grilles.
Nous conjecturons la 2-réductibilité des configurations quelconques sur une grille n*m. Après avoir assimilé les différentes approches possibles du problème, nous attendons du stagiaire qu\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\'il élabore un algorithme intelligent afin d\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\'étudier de manière exhaustive les différentes configurations 4x4, de jouer finement sur ces configurations pour pouvoir ensuite élaborer une éventuelle preuve par induction de cette conjecture. Bien entendu, toute prise d\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\'initiative est la bienvenue, ce stage s\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\'articulant plus comme une expérience du milieu de la recherche.
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 ce problème 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.
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.
URL sujet détaillé :
:
Remarques : Co-encadrement : Laurent Beaudou (doctorant de l'Université Joseph Fourier de Grenoble)
|
|
|
|
|
|
SL307-13 Calcul d'atteignabilité de systèmes hybrides par l'optimisation
|
|
|
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.
Nous allons concentrer notre attention sur une méthode de calcul d'états atteignables, basée sur une extension ensembliste de l'intégration numérique. En plus, l'ensemble d'états atteignables (qui est un sous-ensemble de R^n) est représenté par des contraintes. Le calcul itératif des nouvelles contraintes engendrées par le schéma d'intégration numérique peut être fait par l'optimisation.
L'objectif de ce projet est d'une part d'implanter cette méthode en utilisant de différentes logiciels d'optimisation et ensuite expérimenter l'implantation sur des études de cas de systèmes biologiques. D'autre part, la question théorique à étudier est l'analyse de l'accumulation d'erreurs.
Le candidat devrait avoir des compétences suivantes :
1) Connaissance de base de l'optimisation et de l'analyse numérique
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-opt.txt
Remarques : possibilité de rénumération
|
|
|
|
|
|
SL307-14 Protocoles avec canaux fiables et canaux non-fiables
|
|
|
Description
|
|
Nous nous intéressons aux systèmes communiquant par canaux FIFO non- bornés.Ces systèmes constituent un modèle mathématique pour les protocoles asynchrones.
De façon paradoxale, ils peuvent être en partie analysés automatiquement dans l'hypothèse où les canaux sont non-fiables (c.-à-d. peuvent perdre les messages) alors que, sans cette hypothèse, le modèle a la puissance des machines de Turing.
De façon encore plus surprenante, certains propriétés restent décidables quand le système présente certaines combinaisons de canaux fiables et non-fiables. Par exemple, l'absence de deadlock est décidable dans le cas de réseaux en anneau où chaque participant reçoit les messages de son voisin de gauche et adresse ses messages à son voisin de droite, ceci même si tous les canaux sauf un sont fiables. De même, les questions d'accessibilité alternante (où un participant du protocole cherche à atteindre une configuration et où l'autre participant s'oppose à cet objectif) sont décidables si l'un des canaux est non-fiable.
Objectifs du stage : Pour ce stage de L3 on aimerait parvenir à caractériser la topologie des réseaux combinant canaux fiables et non-fiables, et pour lesquels les questions d'accessibilité sont décidables.
Il s'agit d'un stage où les résultats attendus sont de nature fondamentale, qui s'adresse à un(e) étudiant(e) ayant le goût des preuves formelles et des constructions algorithmiques utilisées dans les résultats d'indécidabilité.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/~phs/l3-07-ps.pdf
Remarques :
|
|
|
|
|
|
SL307-15 Simulation électromagnétique de micro-systèmes RF (RF-MEMS) sur une Grille de calcul
|
|
|
Description
|
|
Des outils précis et rapides sont aujourd'hui utilisés pour la simulation électromagnétique de circuits pour télécommunications à haute densité d'intégration et miniaturisés. Or la complexité grandissante de ces circuits se traduit souvent par des temps d'exécution excessifs. Une approche consiste à implémenter les codes de simulations électromagnétiques sur une Grille de calcul : l'exécution du code électromagnétique est alors distribuée sur plusieurs machines.
L'objectif du stage consistera à simuler sur la grille expérimentale GRID'5000 des micro-systèmes (MEMS) en bande millimétrique. En particulier il s'agira de simuler des déphaseurs contrôlés par un grand nombre de microcommutateurs MEMS et d'analyser les performances de la grille pour ce type de simulations. Ces travaux seront menés en collaboration avec un doctorant travaillant sur le sujet.
URL sujet détaillé :
:
Remarques : - co-encadrant : COCCETTI Fabio
- possibilité d'indemnisation : oui
|
|
|
|
|
|
SL307-16 Dilemme du Prisonnier Itéré et Transition de Phase
|
|
|
Description
|
|
Le probleme du dilemme du prisonnier est un problème classique de théories des jeux.
Il s\'agit ici de s\'interesser a une generalisation de ce probleme, dans le cas ou nous avons n prisonniers disposé sur un graphe quelconque. L\'algorithme qui traduit la formalisation de la stratégie de Pavlov sur ce probleme est un algorithme probabiliste extremement simple et convergent.
L\'objet de ce stage est d\'evaluer le temps de convergence de ce probleme en fonction de la topologie du graphe.
Deux conjectures s\'opposent sur le sujet, l\'une d\'elles evoque meme la possibilite d\'une transition de phase en fonction du degre du graphe.
Il sera demande a l etudiant d\'implementer le probleme (par exemple a l aide d\'un model-checker probabiliste) et de porposer une conjecture, afin de pouvoir ensuite amorcer une preuve formelle.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dcmessika.pdf
Remarques : Co encadré par Brigitte Rozoy.
Possibilité de rémunération à déterminer.
|
|
|
|
|
|
SL307-17 Distribution des nombres flottants dans les registres
|
|
|
Description
|
|
Les processeurs généralistes savent traiter 2 types de représentations des nombres : les entiers (- 1,0,1,2,...) et les nombres à virgule flottante (1.568 E 12, -5.568 E -3, ...). Le processeur effectue des opérations de base (addition, multiplication, division ...) sur ces nombres qui sont stockés dans les registres. Or les architectures modernes ne disposent que de très peu de registre. Aussi lorsque le nombre de registres n'est pas suffisant, certaines valeurs sont renvoyées en mémoire. Ces transferts mémoires sont coûteux en temps mais aussi en consommation électrique.
En effet la mémoire (disque dur, mémoire, cache, registres) d'un ordinateur est caractérisée par la quantité disponible mais aussi par leur bande passante (vitesse à laquelle on va pouvoir écrire ou lire des données dans ces unités de stockage). En réduisant la taille des données qui y transitent ou qui y sont stockées on peut réduire de façon significative la charge de travail d'une machine.
Sur certains processeurs comme les processeurs graphiques, l'information de texture est souvent compressée pour diminuer la quantité d'information qui transite. Parmi les techniques de compression, on utilise souvent le DXTC (DirectX Texture Compression). Cet algorithme consiste à mémoriser 2 couleurs de référence et à utiliser les autres valeurs pour caractériser la quantité de chaque couleur de référence.
Cette technique est naturelle sur les images/textures car l'amplitude de couleurs de pixels adjacents est faible. L'objectif de ce stage est de déterminer si de telles techniques peuvent être mises en place avec les nombres flottants présents dans les processeurs généralistes. Pour cela, il faudra lire les valeurs présentes dans tous les registres flottants après chaque instruction exécutée par le programme cible et caractériser l'amplitude des variations des nombres flottants dans le temps. Les programmes de références à tester seront ceux des SPEC CFP2006 caractéristiques d'applications flottantes s'exécutant sur un processeur généraliste. La lecture des registres se fera à l'aide de l'interface de programmation PIN développée par Intel pour les architectures IA-32 et IA-64.
URL sujet détaillé : http://gala.univ-perp.fr/~ddefour/Stage_ENS_M1_2007.pdf
Remarques :
|
|
|
|
|
|
SL307-18 Développement de la perception couleur d'une rétine biologique simulée.
|
|
|
Description
|
|
Le thème scientifique du projet ODYSEE est l'étude conjointe de la vision algorithmique et de la vision biologique: une meilleure connaissance des mécanismes de perception visuelle humaine et animale pourrait avoir un impact sur la compréhension du cerveau et de ses maladies, mais aussi sur conception d'algorithmes, ou la façon d'interfacer un système artificiel avec des personnes, éventuellement handicapées. Nous étudions ainsi l'activité corticale à un niveau fin en simulant des modèles de groupes de neurones et en reliant ces données aux mesures effectuées en neuro-physio et psychologie.
Dans ce cadre nous avons développé une rétine biologique simulée qui permet de rendre compte à la fois de propriétés statiques et dynamiques du traitement visuel précoce, tenant compte des aspects non-linéaires, dit de contrôle de gain, et des aspects évennementiels, liés au fait que l'information d'un neurone à l'autre n'est pas uniquement liées à des variables continues mais principalement à des "évennements" (décharge des neurones), définissant un codage temporel de l'information.
Dans un soucis de simplicité nous avons volontairement omis de prendre en compte les aspects liés à la couleur et proposons ici de combler cette lacune.
L'étudiant ou le binôme d'étudiant est donc inviter à:
- regarder et faire la synthèse des données bibliographiques sur ce sujet précis, qui lui seront fournies un peu avant le stage
- proposer un modèle pour simuler les effets de la couleur au sein d'une rétine animale ou humaine
- mettre en oeuvre le calcul lié à ce modèle au sein du logiciel C++ existant
en lien avec le doctorant qui a initié et suivi ce projet.
References:
ftp://ftp-sop.inria.fr/odyssee/Publications/2006/wohrer-kornprobst-etal%3A06c.pdf
ftp://ftp-sop.inria.fr/odyssee/Publications/2006/wohrer-kornprobst-etal%3A06b.pdf
http://www.inria.fr/rrrt/rr-5848.html
URL sujet détaillé : http://www-sop.inria.fr/odyssee/team/Adrien.Wohrer/retina/index.html
Remarques : Co encadrement entre Adrien Wohrer, doctorant en fin de thèse et Pierre Kornprobst chercheur permanent
Rémunération d environ 560=80net/mois (selon reglementaton en vigueur)
|
|
|
|
|
|
SL307-19 Analyse et documentation du protocole de synchronisation iSync
|
|
|
Description
|
|
Le système d\'exploitation MacOS X comporte un moteur de synchronisation appelé 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.
Le stage se déroule au sein du projet INRIA-LIP6 Regal http://regal.inria.fr/, qui étudie les systèmes répartis à grande échelle de type P2P. Un de ses axes 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 XVIème arrondissement.
URL sujet détaillé : http://regal.lip6.fr/offresemploi/stages/2007/shapiro-iSync-M1/
Remarques : Ce stage est rémunéré, et pourra éventuellement se prolonger par un stage M2.
|
|
|
|
|
|
SL307-20 Logiques temporelles avec opérateur freeze
|
|
|
Description
|
|
Dans les langages logiques, l\'utilisation de l\'opérateur freeze permet de stocker (geler) des valeurs dans des registres. Ces valeurs peuvent ainsi être réutilisées plus tard dans des modèles qui évoluent au cours du temps. L\'opérateur freeze est une forme restreinte de quantification du premier ordre. Ce mécanisme de stockage et par ailleurs utilisé dans certaines classes d\'automates à registres.
De nombreux travaux récents étudient les propriétés de ce type de logiques. Ici, nous nous intéressons à des extensions de la logique temporelle linéaire LTL avec l\'opérateur freeze. Quelques résultats sont déjà connus et traitent majoritairement le cas où les contraintes permises entre les variables se limitent à l\'égalité. Par exemple, on sait qu\'on peut décider si une formule de LTL augmenté avec des contraintes de répétitions est satisfaisable. On appelle contrainte de répétition une contrainte du type: =93il existe un état futur où la valeur de la variable y est égale à la valeur courante de la variable x=94 (noté x = ◊ y).
D\'une manière générale, LTL avec l\'opérateur freeze est indécidable lorsque l\'on ajoute des comparaisons strictes entre les variables. Il serait intéressant de voir si l\'introduction de relations de comparaisons entre les variables du type x < ◊ y (il existe une future valeur de y plus grande que la valeur courante de x) dans une extension de LTL entraîne déjà l\'indécidabilité. Pour commencer, un domaine d\'interprétation dense et ouvert pour les variables tel que R semble avoir de meilleures propriétés pour une telle extension.
L\'objectif de ce stage consiste d\'abord à se familiariser avec les différents résultats concernant des logiques utilisant l\'opérateur freeze. Puis, on pourra s\'intéresser à la décidabilité du problème de la satisfaisabilité pour l\'extension de la logique LTL évoquée plus haut avec opérateur freeze et comparaisons entre des variables interprétées dans R.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/l3-07-sdrg-1.html
Remarques :
|
|
|
|
|
|
SL307-21 Théorie et mise en oeuvre d'un model-checker de programmes à pointeurs
|
|
|
Description
|
|
Les sources d'erreur de programmation sont multiples. On peut citer à titre d'exemples les débordements d'indices de tableaux, l'utilisation de variables ou pointeurs non initialisés, les divisions par zéro,etc. Certaines des erreurs de programmation sont difficiles à diagnostiquer automatiquement, parce qu'elles touchent au comportement dynamique du programme. C'est le cas en particulier des erreurs liés à l'utilisation de ressources partagées, comme la mémoire.
Afin de vérifier des programmes manipulant des listes simplement chaînées, un algorithme a été proposé dans [2] permettant de traduire le comportement de ces programmes vers des systèmes manipulant seulement des entiers (appelés systèmes à compteurs). L'analyse de ces systèmes à compteurs permet de détecter les erreurs du programme et peut être réalisée par l'outil FAST [1] développé au LSV.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/l3-07-afas-1.html
Remarques : Stage co-encadré par Arnaud Sangnier (LSV).
|
|
|
|
|
|
SL307-22 Etude de la dimension de la solution dans le cadre de l'algorithme de Goemans et Williamson
|
|
|
Description
|
|
L\'algorithme de Goemans et Williamson a de nombreuses applications dans l\'algorithmique, notamment pour le problème de MAXCUT, mais aussi pour bien d?autres questions pratiques. Concrètement, on se fixe un graphe G=(V,E) non orienté, et on calcule la matrice A indéxée
par V={1,...,n} solution du problème:
Maximiser Somme A(i,j) pour (i,j) dans E, avec
- A(i,i)=1 pour i dans {1,...,n}
- A semi définie positive
On s\'interesse ensuite à la racine carrée de A, notée B, i.e. qui vérifie tB B = A.
Les vecteurs colonne de B, notés B1,...,Bn, sont de norme 1.
Quelle est la dimension minimale de vec(B1,...,Bn) pour une solution optimale ?
A dimension contrainte, quelle dégradation a t-on de la solution ?
# Objectifs :
Le stage consistera à lire la bibliographie portant sur le sujet dans un premier temps, puis à étudier le problème.
Ref. M.X. Goemans and D.P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming , J.ACM, 1995,
vol 42, pages 1115-1145.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-23 Random matrix theory for UMTS
|
|
|
Description
|
|
Random matrix theory is a relatively new theory that captures quite
well the information channel capacity for CDMA networks. The goal
of the internship is to translate this results in the UMTS context
where the users can be allocated different rates and powers, with
fairness considerations.
Skills: eigenvector theory, some telecom notions to be acquired
References:
[1] Random matrix theory and wireless communications, by A. Tulino and S. Verdu, now, 2004.
[2] Orthogonal Spreading Code for Quasi-synchronous CDMA Based on Scrambled Walsh Sequence, by K. Choi and T. Han, Globecom 2006.
[3] Capacity Analysis of Downlink CDMA Systems with Quasi-orthogonal Sequences, by S. Cho, B. Jung, and D. Sung, Globecom 2006.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-24 Fairness paradigms for a hotspot WiFi access point
|
|
|
Description
|
|
This intership concerns the access to Internet offered by an access point to a set of users. The goal is to achieve a fair distribution of the ressources based on a game theory approach. In order to prevent the stations from solliciting too much the access point (the uplink) at the expense of the others, the access point will penalize the "bad" stations by offering them in return (in the downlink) a small bandwidth to their internet requests. Friendly stations to the others will receive a fair amount of bandwidth from the access point. The internship will consist in reviewing the litterature on that topic in a first step, and then, with the help of the adviser, new approaches will be considered.
Skills: Linear Programming, duality theory.
References
[1] Cooperation in wireless networks: principles and applications, by Fitzek, Springer 2006.
[2] Leveraging Downlink for Regulation of Distributed Uplink CDMA, by J. Price and T. Javidi.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Guillaume MUNCH : SL307-25 Développement d'un lambda-calcul dual non-déterministe pour la logique classique
|
|
|
Description
|
|
Curien et Herbelin ont montré que la structure du lambda-calcul pouvait être finement analysée au travers d'un calcul symétrique avec opérateurs de contrôle (c'est-à-dire lié à la logique classique). Ce calcul, le calcul lambda-bar, est non-déterministe à la base mais il admet deux sous-calculs duaux, l'un implémentant l'appel par valeur et l'autre l'appel par nom. De son côté, Selinger a exhibé deux structures catégoriques duales pour modéliser les versions appel par nom et appel par valeur du lambda-mu-calcul de Parigot (un calcul classique). Ces modèles sont applicables au cas du calcul lambda-bar. D'un autre côté, Dosen et Petric ont mis au point une structure catégorique caractérisant ce qui semble être l'extension du système mu-mu-tilde avec une opération d'union non-déterministe. Le but du stage est * De caractériser syntaxiquement les réductions valides du système mu-mu-tilde avec union non-déterministe. * D'unifier si possible les présentations catégoriques de Selinger et de Dosen et Petric de telle sorte que, comme dans le cadre syntaxique du calcul lambda- bar, le choix entre non-déterminisme, appel par nom et appel par valeur, se caractérise par la présence ou non d'un axiome particulier au dessus d'un ensemble commun d'axiomes.
URL sujet détaillé : http://pauillac.inria.fr/~herbelin/stages/stage-master-lambda-bar-non-deterministe.html
Remarques : contacts déjà pris; copilotage par Samuel Mimram (PPS)
|
|
|
|
|
|
Rémy BERGASSE : SL307-26 Stratégies d'évolution dérandomisées
|
|
|
Description
|
|
Mots clés:
- algorithmes génétiques
- suites à faible dispersion
- quasi-aléatoire
- stratégies d'évolution
Un code développé dans l'équipe Tao utilise
des routines d'optimisation pour des problèmes
continus pour lesquels les dérivées sont difficilement
accessibles. Les stratégies d'évolution sont un des outils
choisis.
L'équipe travaille dans ce cadre sur le
remplacement de points aléatoires par des points
quasi-aléatoires. Les premiers résultats théoriques et
pratiques, prometteurs, ont donné lieu à publication.
La mise en oeuvre de ces méthodes dérandomisées, leur
étude théorique et/ou expérimentale forment le sujet
de ce stage.
Le stage est destiné à des étudiants intéressés par l'optimisation, qu'ils soient de niveau licence, maîtrise, DEA, master ou stage d'ingénieur.
URLs:
http://www.lri.fr/~teytaud/inriadcma.pdf
http://www.lri.fr/~teytaud/lbeda.pdf
Encadrant : Olivier Teytaud
Contacter Olivier Teytaud (olivier.teytaud.fr)
URL sujet détaillé : http://www.lri.fr/~teytaud/stage5.txt
Remarques : Les stagiaires chez nous sont usuellement rémunérés.
|
|
|
|
|
|
SL307-27>Adding Time to Discrete Models of Genetic Regulatory Networks
|
|
|
Description
|
|
Modeling genetic regulatory network using timed automata as a compromise between the qualitative (purely discrete) and quantitative (differential) level of abstraction.
URL sujet détaillé : http://www-verimag.imag.fr/~maler/stage
Remarques : Co-encadrement avec Gregory Batt, remuneration possible.
|
|
|
|
|
|
Emmanuel LASSALLE : SL307-28 Stratégies probabilistes dans les jeux à deux joueurs
|
|
|
Description
|
|
Description du domaine:
Les jeux d'état finis à deux joueurs apparaissent dans de nombreux problèmes de vérification ou de synthèse de programmes réactifs (contrôle-commandes, protocoles, applications web, etc...). Plus précisément, ces problèmes peuvent être reformulé en des problèmes de résolutions de jeux à deux joueurs.
Par exemple, pour synthétiser un programme qui satisfait une spécification S on peut parfois fabriquer un jeu J(S) dont les stratégies gagnantes pour l'un des joueurs décrivent exactement l'ensemble des programmes satisfaisant la spécification S. On réduit ainsi le problème de la synthèse de programmes à un problème de résolution de jeu ; une correspondance bijective entre les programmes corrects et les stratégies gagnantes assurent la correction de cette réduction.
A travers cette correspondance, on obtient ainsi un modèle abstrait de programme particulièrement simple : un programme est une stratégie, un programme correct est une stratégie gagnante.
Cependant, dans les applications informatiques réelles, la correction des programmes est une propriété souhaitable mais insuffisante ! En effet, un programme doit aussi être efficace (le temps de réponse à une requête doit être par exemple raisonnable), il doit aussi être robuste (la défaillance d'une partie du système doit pouvoir parfois ne pas entraîner de défaillance de l'application), etc...
La question générale qui se pose donc dans ce monde abstrait du paradigme programmes = stratégies est de mettre en évidence d'autres critères que la seule correction permettant d'évaluer la qualité d'un programme.
Quels critères ? Sur quel modèle de stratégie ? Ces questions restent largement ouvertes à l'heure actuelle
Travail demandé:
Une première étude faite au LaBRI, DEA en 2001 [1], a porté sur le modèle des stratégies non-déterministes (à chaque instant plusieurs coups peuvent être autorisées) et d'une forme de robustesse qu'est la notion de permissivité. Cette étude a déjà permis de déblayer le terrain. Ces retombées ont été en un sens spectaculaire puisque qu'un algorithme de calcul des stratégies gagnantes aussi bon que les meilleurs connus alors a pu être ainsi construit.
Dans une approche qui se voudrait encore plus quantitative, on propose aujourd'hui d'étudier la notion de stratégie probabiliste (à chaque instant, les coups autorisés sont affectés d'une probabilité) dans les jeux (non-probabiliste) à deux joueurs. Cette notion vient naturellement comme raffinement de la notion de stratégie non-déterministe.
Le travail de l'étudiant consisterait, dans un premier temps, à faire le lien entre l'étude faites sur les stratégies non-déterministe [1] et les résultats connus sur les stratégies stochastiques [2] et [3].
Dans une deuxième partie, l'étudiant pourrait se consacrer à mettre en évidence, dans le vocabulaire des stratégies probabilistes, des éléments d'évaluations de la qualité de ces stratégies aux titres de l'efficacité, la robustesse, ou d'autre critère encore qui pourrait apparaître.
Si le temps le permet, l'extension de cette étude au cas des jeux distribués [4] pourrait aussi être envisagée.
Mot-clés :
jeu, automate, probabilité, stratégie, processus, correction de programmes, qualité de programmes, système réactifs
Références :
[1] J. Bernet, D. Janin and I. Walukiewicz, Permissive strategies: from parity games to safety games, Theoretical Informatics and Applications (RAIRO), 2002, 36, pp 261 - 275.
[2] K. Chatterjee, L. de Alfaro, T. A. henzinger, The complexity of Stachastic Rabin and Streett Games, ICALP 2005.
[3] K. Chatterjee and T. A. Henzinger, Strategy Improvement for Stochastic Rabin and Streett Games, CONCUR 2006.
[4] J. Bernet, Jeux distribués, thèse de doctorat de l'Université de Bordeaux I, novembre 2006.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-29 Synthèse de fonctions de rang linéaires--Intégration dans FAST
|
|
|
Description
|
|
On s'intéresse à la vérification automatique de propriétés d'inévitabilité pour des systèmes à compteurs. Ces propriétés caractérisent le fait qu'à partir d'un ensemble d'états initiaux, le système ne peut que progresser vers l'ensemble des états inévitables. Pour les systèmes à compteurs, la vérification des telles propriétés est indécidable dans le cas général. En pratique, pour prouver une telle propriété, on cherche à construire une fonction de rang, dépendant du système, des états initiaux et des états inévitables. L'existence de cette fonction garantit que le système vérifie la propriété d'inévitabilité.
La synthèse automatique de fonction de rang est également indécidable dans le cas général. Par contre, le problème devient décidable pour les fonctions de rang linéaires [BMS05] et pour les fonctions de rang linéaires paramétrées [EF07]. Une approche possible consiste à énumérer ces fonctions et à tester pour chacune d'elle si elle est une fonction de rang.
Le but du stage consiste à concevoir un outil logiciel prototype permettant de synthétiser des fonctions de rang pour ces classes de fonctions, et à l'intégrer dans l'outil de modélisation et d'analyse des systèmes à compteurs FAST [BFLP03].
Ce stage comprend quatre parties :
* assimilation du problème de synthèse de fonction de rang, représentation des systèmes à compteurs et fonctions dans l'arithmétique de Presburger.
* développement d'un outil logiciel prototype qui, à partir d'un système à compteurs et d'une propriété d'inévitabilité, construit (si elle existe) une fonction de rang associée.
* application de l'outil sur les études de cas de FAST.
* extension aux fonctions linéaires paramétrées.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/l3-07-afee-1.html
Remarques : Co-encadrant: Alain Finkel, LSV
|
|
|
|
|
|
SL307-30 Implémentation 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: par ordre de difficulté, fonctions hyperboliques inverses, fonctions hypothénuse et racine cubique, fonctions spéciales erf et Gamma.
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 :
|
|
|
|
|
|
SL307-31 Création d'un domaine abstrait adapté aux entiers du langage C
|
|
|
Description
|
|
Dans le cadre de l'analyse statique de programmes par interprétation
abstraite, un bon compromis entre expressivité et coût pour
représenter l'ensemble des valeurs prises par une variable entière
est obtenu en combinant les intervalles et les congruences de
Granger. Dans un tel domaine, il est possible de représenter
exactement les ensembles {0}, {...,-4,-2,0,2,4,...}, {4,12,20,28}.
On conserve des temps de calcul constants pour les différentes
opérations qu'il est nécessaire d'effectuer sur ces ensembles
au cours de l'analyse d'un programme, par opposition avec des
représentations plus précises telles que les unions d'intervalles.
Le stage consistera à définir un domaine abstrait qui soit plus précis
que la combinaison intervalles/congruences, tout en conservant cette
propriété de calcul en temps borné (et court). Le stage pourra selon
les goûts de l'étudiant s'orienter vers la formalisation de propriétés
ou vers l'implémentation, auquel cas une connaissance des jeux
d'instructions vectoriels du type SSE ou Altivec pourrait rendre
l'exercice encore plus intéressant.
La précision attendue de ce domaine abstrait sera particulièrement
orientée vers la modélisation de programmes C écrits avec les idiomes
du code embarqué. Une implémentation éventuelle pourra se placer dans
le cadre de l'outil d'analyse de codes critiques Frama-C développé
en collaboration entre les équipes PROVAL de l'INRIA Futurs, LANDE
de l'IRISA, et au CEA LIST.
Les références bibliographiques nécessaires pour ce stage se trouvent dans
le rapport de master de Stefan Bydge :
http://www.mrtc.mdh.se/publications/1128.pdf
Une bonne connaissance des langages C et Ocaml est attendue.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-32 Protocoles de populations. Modèles et puissance de calcul.
|
|
|
Description
|
|
Domaine du stage
La taille de certains réseaux est maintenant telle, qu'il semble nécessaire de ne plus parler d'individus mais de statistiques, et de proportions. Par exemple, lorsqu'on décrit l'état d'un réseau comme Internet, il n'est pas pertinent de décrire l'état d'un individu donné, mais plutôt de la proportion d'individus dans tel ou tel état. L'évolution du système est alors le fruit d'un jeu, au sens de la théorie des jeux entre les protagonistes.
L'approche qui consiste à remplacer une vision microscopique du comportement de chaque agent par un modèle macroscopique est courante dans les sciences expérimentales, comme en physique, en chimie, en biologie, où une population d'agents (molécules, individus, ...) est abstraite en un certain nombre de quantités continues, dont l'évolution est donnée par une dynamique continue (équation différentielle).
Cette approche est nettement moins courante en algorithmique distribuée.
Alors que, du point de vue de la complexité, les modèles classiques en algorithmique distribuée sont proches des machines de Turing ou des automates cellulaires, cette hypothèse de mobilité passive mène à des modèles qui semblent en différer grandement.
Description détaillée du travail
Angluin et al. ont proposé dans [1] un modèle théorique de calcul inspiré par les calculs par populations. Il vient d'être démontré dans [2] que la version en temps discrète du modèle possède une puissance de calcul qui se caractérise en termes de relations définissables dans une certaine logique (l'arithmétique de Presburger). On peut envisager des extensions naturelles à temps continu du protocole, et de nombreuses variantes dont la puissance reste à comprendre.
L'objectif du travail est précisément de contribuer à comprendre la puissance des modèles obtenus.
Il y a plusieurs points à discuter, selon les goûts du candidat :
=96 expliciter les conditions qui permettent formellement le passage de la description microscopique à une description macroscopique (passage à la limite thermodynamique, dans le langage des sciences expérimentales)
=96 caractériser la puissance de calcul des modèles obtenus. Par exemple, peut-on caractériser la relation de calcul d'entrée sortie du modèle en termes logiques, comme pour le modèle à temps discret?
Références
[1] Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. In Twenty-Third ACM Symposium on Principles of Distributed Computing, pages 290=96299. ACM Press, July 2004.
[2] Dana Angluin, James Aspnes, and David Eisenstat. Stably computable predicates are semilinear. In PODC '06 : Proceedings of the twenty-fifth annual ACM symposium on Principles of distributed computing, pages 292=96299, New York, NY, USA, 2006. ACM Press.
[3] Olivier Bournez. Modèles Continus. Calculs. Algorithmique Distribuée. Habilitation à diriger les recherches, Decembre 2006. http://www.loria.fr/~bournez/HDR/.
URL sujet détaillé : http://www.loria.fr/~bournez/load/sujet-l3-2007.pdf
Remarques : Possibilité d\'une indemnisation de stage. Aucun prérequis nécessaire.On trouvera aussi plus généralement dans les chapitres 2 et 3 de [3] des discussions sur la motivation de ces travaux.
|
|
|
|
|
|
Marc LASSON : SL307-33 Collaboration à l'assistant de preuve PML
|
|
|
Description
|
|
Il s'agit de collaborer sur une partie de l'implantation d'un nouvel assistant de preuve PML. Il s'agit
d'un assistant basé sur un nouveau langage de la famille ML, avec possibilité
de spécifier et prouver des propriétés dans les structures.
Toutefois, le prouver devrait aussi permettre de faire des mathématiques et ceci sans être pénalisé
par la conception au dessus d'un langage de la famille ML. De plus le système de module première classe de PML
devrait très bien convenir aux mathématiques.
L'état actuel de l'implémentation comprends uniquement le langage de programmation PML
(typage + évaluation) écrite en OCaml. Le système de déduction et les spécifications sont en cours
d'implantation.
URL sujet détaillé : http://www.lama.univ-savoie.fr/~raffalli/sujetl3.txt
Remarques : Des discussions avec Pierre Hyvernat qui
participe au projet sont possibles.
|
|
|
|
|
|
SL307-34 Génération non-déterministe d'approximations pour la
|
|
|
Description
|
|
La vérification de programmes est une discipline de l'informatique
qui vise à mettre au point des techniques permettant de valider des
systèmes informatiques, notamment vis-à-vis de leur sécurité. Dans
ce cadre, de nombreux problèmes cruciaux se révèlent cependant
indécidables. Une approche possible est alors d'utiliser des
approximations débouchant sur des semi-algorithmes, c'est-à-dire des
algorithmes ne donnant pas toujours une solution. Le challenge est
ici d'obtenir, en pratique, de bonnes réponses.
Cette approche a été utilisée avec succès au Laboratoire de
l'Université de Franche-Comté, dans le cadre du projet INRIA-CASSIS,
pour la validation de protocoles de communication sécurisés, type ssh.
Dans ce cadre, les techniques d'approximations sont déterministes et
fortement dépendantes du contexte.
L'objectif du stage est d'avoir une approche générale de
génération d'approximation qui ne soit pas déterministe,
c'est-à-dire utilisant de l'aléatoire. En partant d'une démarche
naïve (prendre un état d'automate parmi quelques états possibles pour
approximer le langage) , l'objectif de travail sera de créer, d'affiner et de tester
différentes stratégies afin d'obtenir des approximations pertinentes.
Mots clés : vérification, automates finis, termes, approximation, OCAML.
URL sujet détaillé : http://lifc.univ-fcomte.fr/~kouchna/PresLyon07.pdf
Remarques : Stage co-encadré par Olga
Kouchnarenko et Pierre-Cyrille Héam
Contact :
pour plus de renseignements, n'hésitez pas à contacter Olga
Kouchnarenko (kouchna.univ-fcomte.fr) ou Pierre-Cyrille Heam (heampc.univ-fcomte.fr).
|
|
|
|
|
|
SL307-35 Vérification régulière sur les mots par approximation
|
|
|
Description
|
|
La vérification de programmes est une discipline de l'informatique qui vise à mettre au point des techniques permettant de valider des
systèmes informatiques, notamment vis-à-vis de leur sécurité. Les systèmes à vérifier possèdent souvent, en pratique, un nombre infini d'états possibles. Afin de pouvoir traiter algorithmiquement ces ensembles, il convient de travailler sur des représentations finies. La pratique montre que l'utilisation de langages
réguliers et d'automates finis est très pertinente pour 1)la modélisation et 2)l'analyse de systèmes en utilisant l'analyse d'atteignabilité. Les algorithmes mis en ouvre ont cependant une forte complexité (généralement exponentielle) limitant l'approche à des systèmes de petites tailles.
L'objectif du stage est d'étudier la faisabilité et l'efficacité d'approche algorithmique par approximation. Il s'agira d'adapter aux mots finis une technique existante pour un problème jumeau sur les arbres et de l'élargir en cas de besoin.
Mots clés : Model-checking, Automates, Langages réguliers, Approximations, OCAML
URL sujet détaillé : http://lifc.univ-fcomte.fr/~kouchna/PresLyon07.pdf
Remarques : Stage co-encadré par Olga
Kouchnarenko et Pierre-Cyrille Héam
Contact :
pour plus de renseignements, n\'hésitez pas à contacter Olga
Kouchnarenko (kouchna.univ-fcomte.fr) ou Pierre-Cyrille Heam (heampc.univ-fcomte.fr).
|
|
|
|
|
|
SL307-36 Développement d'un code d'évolution stellaire bidimensionnel
|
|
|
Description
|
|
Le domaine des pulsations stellaires est actuellement très actif, avec les résultats de projets spatiaux attendus dans un avenir très proche (COROT, KEPLER). De telles études permettent non seulement de contraindre la structure des étoiles, mais ont aussi des implications galactiques et extra-galactiques importantes. Certaines étoiles pulsantes (les Céphéides) sont utilisées pour calibrer les distances, ce qui permet de déterminer la constante de Hubble
Les nombreux résultats attendus de ces projets spatiaux destinés à l\\\\\\\'astérosismologie nécessiteront dans un avenir proche des outils théoriques et numériques poussés. L\\\\\\\'interaction entre la convection et la pulsation peut être décrite par des modèles phénoménologiques à une dimension (type longueur de mélange). Ces approches sont cependant très limitées et ont peu de pouvoirs prédictifs. Afin de s\\\\\\\'affranchir de ces incertitudes et de ces modèles phénoménologiques, l\\\\\\\'équipe de l\\\\\\\'ENS du CRAL développe actuellement un code de modélisation numérique multi-dimensionnel (deux dimensions) permettant l\\\\\\\'étude de tels processus.
La résolution des équations d\\\\\\\'évolution stellaire se fait par l\\\\\\\'intermédiaire de systèmes linéaires de grande taille (typiquement 30.000 inconnues). Il est fondamental de trouver des méthodes de résolution robustes et rapides pour ces systèmes.
Les buts de ce stage sont multiples. Il s\\\\\\\'agira en premier lieu de développer une méthode SOR (Successive Over-Relaxation) pour la résolution des systèmes d\\\\\\\'équations. Dans un premier temps, cette méthode sera appliquée à quelques cas test dont les solutions sont connues (advection pure à une et deux dimensions). Il s\\\\\\\'agira entre autres d\\\\\\\'évaluer la rapidité de cette méthode comparativement à d\\\\\\\'autres méthodes déjà testées comme la décomposition LU, de la rendre facilement utilisable si les conditions de son utilisation changent (modification du nombre de voisins pris en compte pour les interpolations aux interfaces des cellules de la grille de calcul). Suivant les résultats obtenus, on pourra envisager d\\\\\\\'implémenter cette méthode dans le code d\\\\\\\'évolution stellaire.
L\\\\\\\'étudiant-e pourra également regarder l\\\\\\\'influence de la manière de discrétiser les équations à résoudre (on peut en général discrétiser une équation donnée de plusieurs manières à un ordre donné), et évaluer l\\\\\\\'importance des conditions aux limites du problème.
Mots clés : analyse numérique, hydrodynamique.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Adrien FRIGGERI : SL307-37 Communautés et dynamique dans les réseaux sociaux
|
|
|
Description
|
|
Les interactions entre humains se modélisent naturellement par des
graphes, souvent appelés 'réseaux sociaux'. Il est bien connu
aujourd'hui que ces graphes ont souvent une structure en communautés,
caractérisée par le fait qu'ils ont une faible densité globale mais
une forte densité locale : il existe des ensemble de noeuds fortement
connectés entre eux alors qu'il y a peu de liens entre ces ensembles.
De plus, ces graphes évoluent au cours du temps : de nouveaux noeuds
et liens apparaissent et disparaissent.
Au delà de ces généralités, nous avons toutefois aujourd'hui peu de
connaissances effectives sur ces structures. Le but de ce stage est
d'approfondir quelques directions particulièrement prometteuses pour
améliorer cette situation. A partir de données réelles, il s'agira
en particulier d'explorer leur structure en communautés (à l'aide
de deux méthodes dont des implémentations sont fournies), et leur
dynamique. L'étudiant sera amené à concevoir des méthodes pour
comparer les structures en communautés et pour décrire des dynamiques
de graphes, problématiques pour lesquels l'existant est quasi nul
malgré le fort besoin exprimé par les applications.
Le travail reposera sur trois ensembles de données qui seront fournis
à l'étudiant : des archives d'une liste de discussion, un ensemble
d'articles du journal 'Le Monde' et les commentaires associés, et
une base de blogs. L'étudiant pourra ainsi entrer immédiatement dans
le vif du sujet.
URL sujet détaillé :
:
Remarques : co-encadrement avec Michel Morvan (CAMS - CNRS et EHESS ; LIP - CNRS et ENS Lyon)
|
|
|
|
|
|
SL307-38 Analyse de sécurité pour JavaScript
|
|
|
Description
|
|
Le but de ce stage est de concevoir et développer un outil générique d'analyse de programmes écrits dans le langage JavaScript.
JavaScript est un langage de programmation simple et répandu, employé notamment pour étendre les plate-formes Mozilla ou Mac OS X. Malheureusement, à l'heure actuelle, la sécurité des applications développées en JavaScript est du type tout ou rien : toute application qui ne s'exécute pas dans l'environnement confiné d'une page web a accès à tous les services proposés par le système d'exploitation, sans contrôle statique ou dynamique.
Le projet Sécurité et Distribution des Systèmes du Laboratoire d'Informatique Fondamentale d'Orléans travaille en ce moment, avec le soutien de développeurs Mozilla, sur une procédure d'analyse du langage JavaScript à l'aide de systèmes de types avec effets. En raison de la complexité des bases théoriques de JavaScript, ce travail passe par l'établissement d'un laboratoire logiciel à l'aide duquel implanter et tester les techniques de vérification de JavaScript.
Ce stage combine théorie des langages de programmation, théorie de la compilation et programmation appliquée. Les objectifs du stage seront les suivantes :
* rassembler les spécifications complètes du langage JavaScript
* à l'aide de techniques de compilation de langages fonctionnels et par objets, spécifier et implanter une bibliothèque d'analyse syntaxique et de résolution de symboles pour JavaScript
* à partir de cette bibliothèque, implanter un outil générique d'analyse comparable à Uno [1]
* employer cet outil pour valider expérimentalement le système de types de Christopher Anderson pour JS0 [2].
Pour l'implantation, le stagiaire est invité à employer un langage de programmation fonctionnelle de son choix, si possible OCaml, Haskell ou une extension d'un de ces langages. À terme, si le projet et les recherches qui l'accompagnent se déroulent comme prévu, l'outil ainsi développé servira de prototype à une extension de la plateforme Mozilla destinée à vérifier automatiquement la sûreté des extensions téléchargées. Ce projet est entrepris avec l'aide des développeurs de Mozilla. Le stagiaire pourra donc compter sur l'aide distante de plusieurs développeurs de Mozilla -- et, avec un peu de chance, du concepteur originel de JavaScript.
[1] http://spinroot.com/uno/
[2] http://pubs.doc.ic.ac.uk/chrisandersonphd/
URL sujet détaillé : http://www.univ-orleans.fr/lifo/Members/David.Teller/research/enslyon2007/stage.pdf
Remarques :
|
|
|
|
|
|
Raphaël DONZEL : SL307-39 Algorithme parallèle d'extraction de fond sur carte graphique
|
|
|
Description
|
|
De nombreuses applications de vision par ordinateur nécessitent d'extraire, dans un premier temps, la partie intéressante de l'image. Une méthode consiste à supposer que l'on dispose d'un fond statique et d'extraire automatiquement les zones correspondant aux
nouveaux objets (avant plan). Une solution très utilisée dans l'audiovisuel (par exemple pour la météo), dénommée chroma-keying,
repose sur l'utilisation d'un fond de couleur uniforme et en la détection de cette couleur dans les images. Des solutions moins contraignantes ont aussi été proposée par la communauté de la vision par ordinateur. Elles reposent sur l'apprentissage d'un modèle statistique du fond supposé fixe et sur la comparaison de chaque pixel à ce modèle. Ces techniques souffrent cependant de problèmes de
robustesse ou de temps de calcul prohibitifs. En effet pour améliorer les résultats, plus d'informations doivent être intégrées nécessitant
alors beaucoup plus de calculs.
L'objectif de ce stage est d'étudier de nouvelles techniques d'extraction de fond et d'en faire
une implantation parallèle efficace sur carte graphique. Ce travail s'intégre plus largement
dans le cadre des travaux menés entre l'équipe Moais et Perception en réalité virtuelle et augmentée autour de la plateforme grimage (http://www.inrialpes.fr/grimage) où l'extraction de fond est une étape critique pour la reconstruction 3D.
Le travail se fera en trois phases :
- Amélioration de la méthode d 'extraction en prenant en compte les bonnes informations. Cela passe donc par un travail de bibliographie, puis par la définition d'une mesure de qualité. Cette mesure permettra ainsi de comparer les différentes
techniques et ainsi d'extraire les informations qui apparaissent comme les plus importantes.
- Implantation parallèle de l'algorithme sur carte graphique Nvidia 8800 en utilisant
l'environnement Cuda (http:/developer.nvidia.com/object/cuda.html). Ce type de calculs (indépendants par pixel) se prêtent parfaitement à ces nouvelles architectures parallèles.
- Intégration dans la chaine de reconstruction 3D et tests en situation réelle sur la plateforme Grimage.
Thanarat Horprasert and David Harwood and Larry S. Davis. A Statistical Approach for Real-time Robust Background Subtraction and Shadow Detection IEEE ICCV'99 frame-rate workshop.
German Cheung and Takeo Kanade and Jean-Yves Bouguet and Mark Holler. A real time system for robust 3D voxel reconstruction of human motions. CVPR00.
J. Shen. Motion detection in color image sequence and shadow elimination. Proceedings of SPIE, Visual Communications and Image Processing 2004.
URL sujet détaillé :
:
Remarques : Co-encadrants:
Edmond Boyer: edmond.boyer.fr
Clement Menier: clement.menier.fr
Le stagiaire sera indemnise (montant minimum 310 euros par mois)
|
|
|
|
|
|
Pascal VANIER : SL307-40 Probabilités de conflicts dans un graphe de flot de contrôle
|
|
|
Description
|
|
Ce stage se place dans le cadre d'une collaboration entre l'équipe Compilation et systèmes embarqués (Compsys) du LIP et l'équipe Compiler-Expertise-Center (CEC) de ST-Microelectronics.
Les processeurs ST200 comportent un cache d'instructions direct-mapped avec un coût d'un défaut de cache de 150 cycles.
Il convient donc d'optimiser finement le placement des instructions en mémoire.
L'algorithme de placement utilise un graphe dit de conflit où les sommets représentent des blocs d'instructions et où chaque arête pondérée traduit le coût de faire partager une même ligne de cache aux deux blocs d'instructions correspondant. Actuellement, le graphe de conflit est construit à partir d'une trace d'exécution (approche dynamique) obtenue par profiling.
Le problème du profiling est triple : le processus de compilation est trop complexe pour la majorité des développeurs. Aussi le temps de compilation est relativement coûteux. Finalement, le choix de l'ensemble de données utilisées pour nourrir le programme lors du profiling est parfois crucial.
L'approche statique (analyse symbolique lors de la compilation) ou même mixte est ainsi préférée par les développeurs. Seulement générer un bon graphe de conflit à partir de probabilités de branchement est un problème encore ouvert.
Le but du stage est de résoudre ce problème c'est à dire être capable de générer un graphe de conflit en un temps raisonnable (par calcul symbolique et/ou relaxation) à partir d'un graphe de flot de contrôle dont les probabilités de branchement ont déjà été calculées (chaîne de Markov à pile).
URL sujet détaillé : http://perso.ens-lyon.fr/benoit.boissinot/Licence_2007_cache.pdf
Remarques : Co-encadrement avec Fabrice Rastello
|
|
|
|
|
|
SL307-41 Outils pour la programmation monadique en Coq
|
|
|
Description
|
|
Le système de démonstration sur ordinateur Coq fournit un langage de programmation fonctionnel que nous utilisons pour décrire des algorithmes avant de prouver leur correction. Le caractère fonctionnel pur de ce langage interdit d'utiliser certaines structures de programmation, comme l'affectation de variables modifiables ou la levée d'exception, ou les deux; pourtant ces structures de programmation permettent souvent de construire des programmes plus efficaces, avec une gestion plus fine de la mémoire ou du contrôle. Une approche systématique pour simuler ces structures de programmation est de coder les variables modifiables et les exceptions par un style de programmation systématique basé sur une notion de monade, c'est-à-dire la combinaison d'une transformation systématique sur les types de données, accompagnées d'opérateurs spécifiques pour gérer la composition des fonctions.
L'approche systématique fournie par les monades implique que les démonstrations de correction des algorithmes prennent aussi une forme qui est systématiquement la même. Le but du stage est d'isoler les techniques de preuve qui s'adaptent aux programmes basés sur des monades et de programmer les procédures d'aide à la preuve qui supportent ces techniques et permettent d'améliorer l'efficacité du travail de démonstration sur ordinateur.
Robert S. Boyer, J Strother Moore, single-threaded objects in ACL2, 1999
http://citeseer.ist.psu.edu/boyer99singlethreaded.html
Nick Benton, John Hughes, and Eugenio Moggi
"Monads and effects", Applied semantics, G. Barthe, P. Dybjer, L. Pinto, J. Saraiva (Eds.), Springer Verlag, LNCS 2395, 2002. http://www.disi.unige.it/person/MoggiE/APPSEM00/
Yves Bertot, Pierre Castéran
_*Interactive Theorem Proving and Program Development: /Coq'Art: The Calculus of Inductive Constructions/*_, Springer Verlag, EATCS Texts in Theoretical Computer Science, ISBN 3-540-20854-2, 2004
URL sujet détaillé :
:
Remarques : Une rémunération est possible, mais un seul étudiant pourra être rémunéré sur les différents stages proposés dans l'équipe Marelle.
|
|
|
|
|
|
SL307-42 Implémentation certifiée et itérative de la racine Carrée dans le style de Karatsuba.
|
|
|
Description
|
|
Dans un travail de 1998, P. Zimmermann a fourni une fonction de racine carrée pour la bibliothèque GMP qui utilise de façon spectaculairement efficace les propriétés des représentations usuelles des grands nombres entiers. Cette fonction a la propriété de travailler pratiquement en mémoire constante, grâce à un approche en "diviser pour règner" et à un choix judicieux des portions de mémoire où sont stockés les résultats intermédiaires.
L'algorithme de P. Zimmermann a fait l'objet d'une preuve formelle de correction vérifiée à l'aide de Coq. Cette preuve formelle contient plusieurs niveaux et en particulier la propriété de mémoire constante à été vérifiée partiellement, en se concentrant sur le tableaux qui conserve les chiffres du nombre en entrée, les résultats intermédiaires, et le résultat final.
Toutefois, la propriété "mémoire constante" n'est pas entièrement satisfaite, car le programme utilise une pile d'appel pour la récursion et il reste la question de savoir s'il est possible de rendre le programme itératif au lieu de récursif, pour faire disparaitre le besoin de cette pile d'appel. Nous proposons de faire l'étude d'une variante itérative de l'algorithme, en implémentant cette variante à l'aide de la bibliothèque GMP, en comparant l'efficacité de la variante avec l'algorithme existant, et en prouvant formellement la correction de la nouvelle variante.
Les étudiants candidats devront connaître les notions de bases de la programmation en C pour l'arithmétique des ordinateurs et avoir un intérêt pour la preuve de programme en utilisant Coq ou les outils de la suite why/caduceus.
Références
Yves Bertot, Nicolas Magaud, and Paul Zimmermann,
``A Proof of GMP Square Root'', /Journal of Automated Reasoning/ 29(3-4):225-252, 2002. Special Issue on Automating and Mechanising Mathematics: In honour of N.G. de Bruijn
(version préliminaire : http://www.inria.fr/rrrt/rr-4475.html)
Yves Bertot,
``Vérification formelle d'extractions de racines entières'', Technique et science informatiques, 24(9), pp. 1161--1185, 2005
Yves Bertot, Pierre Castéran
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer Verlag, EATCS Texts in Theoretical Computer Science, ISBN 3-540-20854-2, 2004
URL sujet détaillé :
:
Remarques : Une rémunération est possible, mais un seul étudiant pourra être rémunéré sur les différents stages proposés dans l'équipe Marelle.
|
|
|
|
|
|
Loïc MAGNAN : SL307-43 Optimisation et fusion de calculs sur FPGA
|
|
|
Description
|
|
Les circuits reconfigurables (ou FPGA pour Field-Programmable Gate
Array) sont des circuits programmables comme les micro-processeurs,
mais à un grain beaucoup plus fin : celui de la porte logique. Depuis peu, ces circuits sont distribués comme co-processeurs dans certains
supercalculateurs (Cray ou SGI). Ils sont particulièrement adaptés à l'accéleration de calculs exotiques à grain fin (cryptographie,
séquençage, analyse d'image...). Toutefois, avec les progrès de l'intégration, on se met à publier des applications d'accélération de calculs flottants, domaine roi du microprocesseur classique.
Le but de ce stage est de contribuer à une telle application dans le domaine biomédical: la simulation du champ magnétique ponctuel produit
par un ensemble de bobines. On dispose pour cela d'un code Matlab en virgule flottante simple précision, comportant les quatre opérations,
la racine carrée et le logarithme. Nous disposons dans l'équipe Arénaire de tous ces opérateurs (en VHDL), et une simple transposition de ce code sur le FPGA est donc possible. Ce n'est toutefois pas
complètement trivial, car il faut ordonnancer les calculs, harmoniser les pipelines, minimiser l'occupation mémoire intermédiaire, et tenir
compte des contraintes de capacité du FPGA.
Toutefois, si le temps le permet, le but de ce stage est de faire mieux. En effet, la flexibilité du FPGA permet en principe
d'optimiser des opérateurs dans leur contexte. D'abord, on peut faire varier la précision des calculs: 24 bits de mantisse (simple précision) ne sont sans doute pas nécessaires partout. Une analyse d'erreur montrera d'ailleurs peut-être qu'ils ne sont pas suffisants partout. Ensuite, on peut spécialiser des opérateurs. Par exemple,
dans le calcul d'une norme en virgule flottante, on a deux multiplications qui sont des carrés (et nécessitent donc moins de travail que de vraies multiplications), suivies d'une addition de ces
carrés, qui sont toujours positifs: à nouveau, cette information permet de simplifier l'additionneur à utiliser. On aimerait enfin
fusionner des opérateurs, toujours connaissant leur contexte. L'équipe Arénaire a en particulier développé une expertise unique sur l'approximation d'une fonction par un polynôme, que l'on pourra
chercher à appliquer au code Matlab à étudier.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-44 Construction des groupes extrémaux
|
|
|
Description
|
|
Dans le cadre de la formalisation du théorème de Feit-Thompson sur la théorie des groupes basée sur l'approche ssreflect (déjà utilisée par G.
Gonthier pour le théorème des 4 couleurs), nous devons construire et classifier les groupes extrémaux, c'est-à-dire les 0groupes presque cycliques (plus précisément, d'ordre ^n un cycle d'ordre ^{n-2}502 80 79 81 502.
Le travail à effectuer sera de construire ces groupes (groupes modulaires, dihédraux et quaternions généralisés), d'établir leurs relations caaractéristiques, et d'en déduire la classification de leurs sous-groupes et automorphismes. Ce travail s'appuyera sur la plateforme de théories des groupes développée par l'équipe "Composants mathématiques" du Centre de Recherche commun Inria-Microsoft Research, et comportera un part importante de démonstration sur ordinateur.
Le candidat devra maîtriser la programmation fonctionnelle typée telle qu'on la pratique en Ocaml ou en Haskell. De bonnes connaissances en mathématiques, soit en ce qui concerne l'algèbre, soit en ce qui concerne la logique et ses relations avec les langages de programmation et la preuve sur ordinateur seront également appréciés.
URL sujet détaillé :
:
Remarques : Stage rémunéré
Co-encadré par Assia Mahboubi
|
|
|
|
|
|
Fabien GIVORS : SL307-45 Machines de Turing et entropie topologique
|
|
|
Description
|
|
Le calcul de l\'entropie d\'un système dynamique est souvent difficile. Celà est teimogné par le fait qu\'on sait calculer, de manière précise, l\'entropie seulement d\'un petit nombre de systèmes dont, par exemple, certains automates cellulaires ou les sous-shifts sofiques. De plus, en litterature commencent à apparaître un certain nombre de résultats montrant que pour certains systèmes, l\'entropie est non-calculable.
Le but du stage est d\'étudier la calculabilité de l\'entropie des machines de Turing en s\'inspirant des travaux [DB] et [S].
Il s\'agira d\'abord de comprendre la notion d\'entropie topologique pour les systèmes dynamiques discrets. Etudier le cas du shift et quelques systèmes liés. Ensuite, en s\'inspirant des techniques de [S], il faudra voir s\'elles sont généralisables aux Machines de Turing.
Ce stage ne demande aucun prérequis particulier sinon un goût
pour le formalisme et une bonne dose de fantaisie.
[S] J.G. Simonsen. On the computability of the topological entropy of subshifts. DMTCS vol 8:83-95, 2006.
[DB] J.-C. Delvenne and V.D. Blondel. Quasi-periodic configurations and undecidable dynamics for tilings, infinite words and Turing machines. Theoretical Computer Science, 319:127-143, 2004.
URL sujet détaillé :
:
Remarques : Possibilité de poursite en thèse. Possibilités de rémuneration sous certaines conditions.
|
|
|
|
|
|
SL307-46 Automates cellulaires asynchrones
|
|
|
Description
|
|
L'implementation de systèmes de simulation d'agents agissants et inter-agissants de manière asynchrone demande toujours une notion d'ordonnancement. Il est clair que le fonctionnement de l'ordonnanceur peut grandement affecter le comportement global du système.
Recemment, Mortveit et Reidys ont proposé de modéliser ces systèmes d'agents asynchrones par les systèmes dynamiques
discrets séquentiels [MR]. Dans [HMR], ils étudient le cas dans
lequel l'évolution du système est indépendante de l'ordonnanceur.
Dans ces études, le système est toujours considére comme étant formé d'un nombre fini d'agents. Le but du stage consiste à généraliser le formalisme au cas d'un nombre infini d'agents et de voir ce qui en reste des résultats de [HMR] dans ce cas.
Le stage ne demande aucun prérequis particulier sinon une conaissance de base dans les domaines fondamentales de l'informatique. Un goût pour le formalisme et une bonne dose de fantaisie seront sans doute des atout majeurs.
Bibliographie.
[MR] H.S. Mortveit and C.M. Reidys. Discrete sequential dynamical systems. Discrete Mathematics 226:281-295, 2001.
[HMR] A.A. Hanson, H.S. Mortveit and C.M. Reidys.
On asynchronous cellular automata. Advances in complex systems 8(4):521-538, 2005.
URL sujet détaillé :
:
Remarques : Possibilité de poursite en thèse. Possibilités de rémuneration sous certaines conditions.
|
|
|
|
|
|
SL307-47 Automates cellulaires et contrôle
|
|
|
Description
|
|
Dans les systèmes dynamiques classiques, pour simuler certaines phénomes, il est indispensable tenir compte de certaines données qui viennent de l'extérieur du système et qui ne modifient le comportement.
Prenons un exemple pratique. Considérons une voiture sur une autoroute. Une fois que la voiture est lancée, et l'accelerateur
appuye, le "système voiture" maintient une certaine direction
indéfiniment (enfin, tant qu'il y a du carburant, bien sûr). Le conducteur intervient de temps en temps sur le système pour
corriger la direction de marche (ou éviter des obstacles). Après un
certain temps la voiture arrive à destination et elle s'arrête (situation d'équilibre du système).
Dans le "système voiture", le conducteur joue le rôle du "contrôle"
et modifie le comportement final du système pour l'amener à un certain point d'équilibre possiblement different de celui sur lequel serait tombé sans l'apport du contrôle.
Le but du stage est d'étudier un formalisme pour introduire la notion de contrôle dans le cadre des automates cellulaires. Une première approche est proposée dans [EYEJA]. Cet approche a le défaut de prendre l'état des AC sur les nombres réels. Nous voudrions introduire un nouveau formalisme qui relaxe cette condition. Il sera intéressant ensuite de commencer à explorer cette nouvelle classe de systèmes dynamiques et commencer à en décrire les comportements, au moins les plus simples.
Ce stage ne demande aucun prérequis particulier sinon une bonne dose de fantaisie. Un goût pour le formalisme et une bonne conaissance des domaines fondamentaux de l'informatique seront sans doute des atouts majeurs.
Bibliographie.
[EYEJA] S. El Yacoubi, A. El Jai, N. Ammor. Regional Controllability with Cellular Automata Models. In S. El Yacouby and B. Chopard, editors, Cellular automata for research and industry (ACRI'06), volume 4173 of Lecture Notes in Computer Sciences, pag. 676-685, September 20-23, Perpignan (France), 2006.
URL sujet détaillé :
:
Remarques : Possibilité de poursite en thèse. Possibilités de rémuneration sous certaines conditions.
|
|
|
|
|
|
Pierre-Etienne MEUNIER : SL307-48 Complexité dans les pavages
|
|
|
Description
|
|
Il s'agit d'étudier la reconnaissance de langages par des pavages.
Les pavages sont des objets 2D décrit par une structure locale simple. Bien qu'il s'agisse d'objets statiques, il est toutefois possible de reconnaitre des langages (voir sujet détaillé).
On s'intéresse ici à démontrer quelques propriétés élémentaires de cette notion de reconnaissance, ainsi qu'à étudier le lien avec les automates cellulaires non déterministes.
URL sujet détaillé : http://www.lif.univ-mrs.fr/~ejeandel/interns.html
Remarques :
|
|
|
|
|
|
SL307-49 Bords dans les pavages
|
|
|
Description
|
|
Les pavages sont des images en deux dimensions régies par des règles locales
simples.
On s'intéresse à caractériser certains pavages par leur "bordure" : les
bordures d'un pavage sont tous les bords des carrés que contient ce pavage.
Pour étudier les bordures, on s'intéresse ici à une relation d'ordre naturelle sur les pavages induite par les bordures (voir sujet détaillé).
Le but du stage est ainsi de donner quelques propriétés de cet ordre et de les relier à d'autres notions déjà connues.
URL sujet détaillé : http://www.lif.univ-mrs.fr/~ejeandel/interns.html
Remarques :
|
|
|
|
|
|
SL307-50 Distribution de calculs pour résoudre le dilemme du fabricant de tables
|
|
|
Description
|
|
Afin de résoudre le dilemme du fabricant de tables[1] pour certaines fonctions élémentaires en double précision, de nombreux calculs doivent être effectués et lancés sur le plus grand nombre de machines possibles. Les calculs sont indépendants et ne nécessitent pas de communication entre les machines de calcul, les résultats devant juste être centralisés pour être filtrés puis stockés sur disque.
Un petit système client-serveur a été écrit, mais le système actuel a ses limitations: par exemple, les communications entre le client et le serveur ont juste pour but de distribuer les calculs, la centralisation des résultats se faisant soit automatiquement grâce à NFS, soit par synchronisation avec Unison. D'autre part, l'utilisation actuelle de Maple empêche d'effectuer certaines parties des calculs sur les machines ne possédant pas Maple.
Pour ces raisons, un nombre limité de machines est actuellement utilisé: les serveurs de calcul du LIP, un cluster et une machine personnelle.
Le but du stage est d'analyser les besoins à court et à long terme, de proposer une solution et de l'implémenter. Quelques pistes possibles:
_ Écriture d'une interface avec un autre système de distribution de calculs, comme BOINC[2].
_ Faire passer le filtrage mentionné au premier paragraphe dans la partie distribuée. Le filtrage actuel utilisant le logiciel Maple, un passage à la bibliothèque MPFR[3] est nécessaire.
Prérequis: ils dépendent de la solution choisie. Par exemple, des connaissances de base sur Unix seront nécessaires à l'écriture d'une interface entre divers outils. Les programmes de ce projet étant écrits en Perl, une connaissance du langage Perl est un plus, voire nécessaire si ces programmes doivent être modifiés.
Une description détaillée du problème et des programmes d'origine est donnée dans: V. Lefèvre. Moyens arithmétiques pour un calcul fiable. PhD thesis, École Normale Supérieure de Lyon, Lyon, France, janvier 2000.
Prendre contact avec Vincent Lefèvre pour de plus amples renseignements.
[1] http://perso.ens-lyon.fr/jean-michel.muller/Intro-to-TMD.htm
[2] http://boinc.berkeley.edu/
[3] http://www.mpfr.org/
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-51 Analyse comparative des mécanismes de
|
|
|
Description
|
|
L'objectif de ce stage est d'analyser les différentes techniques de " backtracking " (dits aussi traceback) et de filtrage de paquets qui visent à traquer et éliminer les paquets fautifs dus à des attaques de déni de service (DoS, DDoS).
Ce travail s'inscrit dans le cadre d'un projet de recherche CNRS multi-disciplinaire, appelé METROSEC, dont l'objectif ultime est d'augmenter la robustesse et l'insensibilité du réseau vis-à-vis des ruptures dans le trafic et la topologie du réseau (dues à des attaques de déni de service) afin qu'il puisse continuer de fournir un service acceptable et de garantir la qualité de service demandée (voir http://www.laas.fr/METROSEC/ pour plus d'information).
Voir description détaillée du sujet dans rubrique "URL du sujet détailé"
URL sujet détaillé : http://petitcharlie.essi.fr/~karima/sujet_MetroSec_Stage_2006.doc.pdf
Remarques : Stage rémunéré
|
|
|
|
|
|
SL307-52 Amélioration de la bibliothèque fplll
|
|
|
Description
|
|
Un réseau Euclidien est un sous-groupe discret de R^n pour un certain n, ou encore l'ensemble des combinaisons linéaires entières de vecteurs linéairement indépendants, appelés base. La discrétude implique l'existence d'un vecteur non-nul de longueur minimale. Calculer un tel vecteur à partir d'une base quelconque est NP-difficile lorsque la dimension augmente (sous des réductions probabilistes), aussi se contente-t-on souvent d'un vecteur qui n'est pas nettement plus long. L'algorithme LLL, créé par Arjen et Hendrik Lenstra et Laszlo Lovasz en 1982, permet d'obtenir un vecteur de longueur inférieure à ^d la longueur minimale. Cela s'avère
suffisant pour de très nombreuses applications, en cryptographie, en théorie algorithmique des nombres, en calcul formel, etc.
Dans la pratique, lorsque l'on veut LLL-réduire une base, les codes les plus efficaces sont ceux de la bibliothèque NTL de Victor Shoup [1] et du système de calcul MAGMA [2]. Le premier a les inconvénients d'être plus lent et de nécessiter une certaine familiarité avec les réseaux de la part de l'utilisateur. Le second est plus rapide, mais il n'est pas libre : le code n'est pas disponible et ne peut donc pas être modifié et étudié par l'utilisateur. Il existe un compromis, fplll-1.3 [3], à partir duquel a été élaboré le code de MAGMA et qui est libre. fplll-1.3, bien qu'utilisé, n'est pas très populaire car il n'est pas simple d'utilisation.
Après une familiarisation avec les réseaux euclidiens et l'algorithme LLL, l'étudiant aura pour mission de rendre le code fplll-1.3 plus simple d'utilisation, en automatisant la politique de choix entre les différentes variantes heuristiques et prouvées. Il s'agira aussi d'améliorer autant que possible le code. Cela comblerait un manque sérieux pour les utilisateurs de l'algorithme LLL, à savoir la présence d'une implantation libre, simple d'utilisation et efficace.
L'algorithmique des réseaux euclidiens est complexe à la fois du point de vue mathématique et informatique. Ainsi, ce stage est donc destiné à un étudiant avec à la fois un bonne capacité d'abstraction, et un goût prononcé pour la programmation.
Bibliographie:
[1] http://www.shoup.net/ntl/
[2] http://magma.maths.usyd.edu.au:8000/
[3] http://perso.ens-lyon.fr/damien.stehle/downloads/fplll-1.3.tar.gz
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-53 Racines d'automates cellulaires
|
|
|
Description
|
|
Un automate cellulaire est un modèle de calcul parallèle synchrone, qui peut être vu comme un système dynamique (A^Z, F), où A est un ensemble fini d'états et F est continue de A^Z dans A^Z. La dynamique de F^k est en quelque sorte incluse dans la dynamique de F. En revanche, on ne sait pas si, étant donné F^k, on peut retrouver la forme de F (trouver une racine k-ième). Ce stage aura pour premier but de comprendre les racines carrées de l'automate cellulaire identité. Ensuite, on s'attaquera éventuellement à des automates cellulaires plus compliqués.
URL sujet détaillé :
:
Remarques : stage coencadré par Pierre Guillon
|
|
|
|
|
|
SL307-54 Distances compatibles avec les Automates Cellulaires
|
|
|
Description
|
|
Les automates cellulaires sont un modèle de calcul parallèle synchrone. Il sont étudiés en tant que système dynamique dans différentes topologies sur A^Z (où A est l'ensemble fini de ses états). Les plus utilisées sont la topologie de Cantor, qui prend en compte une fenêtre finie sur les configuration, ou la topologie de Besicovitch, qui prend en compte la densité globale de défauts sur la configuration. Le but de ce stage sera de caractériser les topologies "intéressantes" au point de vue des automates cellulaires, en commençant par les topologies pseudo-métriques.
Référence: F.Blanchard, E.Formenti et P.Kurka. Cellular automata in Cantor, Besicovitch and Weyl topological spaces. CS 11(2):107-123, 1999.
J.Cervelle, B.Durand and E.Formenti. Algorithmic information theory and cellular automata dynamics.
LNCS 2136, 2001.
URL sujet détaillé :
:
Remarques : stage coencadré par Pierre Guillon
|
|
|
|
|
|
SL307-55 Expansivité des Automates Cellulaires
|
|
|
Description
|
|
Un automate cellulaire est un modèle de calcul parallèle synchrone, qui peut être vu comme un système dynamique (A^Z, F), où A est un ensemble fini d'états et F est continue de A^Z dans A^Z. Il est expansif (pour la topologie de Cantor) si toute différence entre deux configurations finira par se répercuter au milieu. Une classe importante d'automates cellulaires expansifs est la classe des permutifs. Le but de ce stage sera de comprendre le lien étroit entre expansifs et permutifs, et notamment construire des automates cellulaires qui soient expansifs mais pas permutifs.
Référence: F.Fagnani, L.Margara. Expansivity, Permutivity, and Chaos for Cellular Automata. TCS vol 31, 1998.
P.Kurka. Topological and Symbolic Dynamics. SMF.
URL sujet détaillé :
:
Remarques : stage coencadré par Pierre Guillon
|
|
|
|
|
|
SL307-56 Protocoles réseaux tolérants aux coupures pour les Grilles à grande échelle (Disruption
|
|
|
Description
|
|
L'objectif de ce stage est de proposer, d'adapter et de valider des solutions pour le support des réseaux tolérants aux délais et aux coupures ("Delay and Disruption Tolerant Networks (DTN)") dans le cadre des Grilles à grande échelle de calculs et de données.
Pendant le stage, l'étudiant prendra en main la couche "bundle" fournie par la communauté DTN (package dtn2). Puis, il proposera une
architecture de passerelle autonome programmable ("Autonomic Programmable Gateway") apte à supporter les protocoles DTN lors de
transfert de données dans les Grilles. L'architecture de passerelle sera implémentée dans une "Linux Box".
Le stagiaire utilisera des outils existants pour simuler les latences et les déconnections dans les réseaux longue distance. En se basant sur des outils logiciels d'emulation reseaux (nistnet, dummynet...), l'etudiant devra analyser et adapter les capacités de ces outils pour supporter de très longues latences réseaux, des interruptions et des
bandes passantes hétérogènes.
L'étudiant devra ensuite mettre en oeuvre un système d'émulation réseaux capable de réagir à des commandes simulant des déconnections.
Une partie du stage concernera la validation de l'approche et la mesure de performances avec différents scénario. Ce projet sera
validé sur la plate-forme Grid5000.
Ce stage nécessite de bonnes compétences en C et programmation système.
Ce stage se place en lien avec les travaux sur la Grille inter-planétaire menés par l'équipe RESO. Quelques informations préliminaires sur la passerelle autonome sont disponibles a:
http://perso.ens-lyon.fr/laurent.lefevre/Papers/SMCIT06_Lefevre_Gelas.pdf
References :
- DTN Research Group : http://dtnrg.org
URL sujet détaillé :
:
Remarques : Co-encadrement : Jean-Patrick Gelas, Equipe RESO / LIP
http://perso.ens-lyon.fr/jean-patrick.gelas/
|
|
|
|
|
|
SL307-57 Etude et proposition d'un noeud reseaux d'experimentation autour d'une plate forme DSL
|
|
|
Description
|
|
L'objectif de ce stage est de proposer et valider un environnement complet pour des machines a capacités limitée déployées autour d'infrastructures DSL. Ce stage devra proposer des solutions pour déployer facilement et de manière sécurisée des expérimentations sur
ces noeuds réseaux. Il devra aussi prendre en compte la remontée d'informations venant des noeuds.
La solution finale proposée dans le cadre du stage sera validée sur un système GNU/Linux minimal basé sur une carte mère au format mini-ATX, fanless et pourvu d'une carte Compact Flash (CF) en lieu et place d'un disque dur traditionnel.
Le stagiaire deploiera et expérimentera une plate-forme de noeuds réseaux autour d'un réseau ADSL.
Ce stage se place dans le cadre du projet DSLLAB.
http://www.lri.fr/~rezmerit/dsllab/index.html
DSLlab est un projet complémentaire à PlanetLab et Grid5000, qui vise à offrir à la communauté de chercheurs sur les systèmes de mutualisation de ressources l'outil adéquat pour comprendre l'impact des réseaux de type ADSL.
Dans le cadre de ce projet, seront placés chez des particuliers (chercheurs et collaborateurs), au sein de leur réseau domestique, des ordinateurs
personnels de faible consommation, faible encombrement et faible nuisances sonores, disponibles de manière permanentes pour lancer des
expérimentations.
L'étudiant choisissant ce stage doit avoir une bonne connaissance de Linux et des outils open source.
URL sujet détaillé :
:
Remarques : Co-encadrement : Jean-Patrick Gelas, Equipe RESO / LIP
http://perso.ens-lyon.fr/jean-patrick.gelas/
|
|
|
|
|
|
Bruno GRENET : SL307-58 Ordres partiels monotones
|
|
|
Description
|
|
On considere un ensemble d'applications f1, f2, ... fk
de A vers A (A est un ensemble fini ou denombrable).
Le but est de trouver un algorithme qui permette de construire une relation d'ordre partiel sur A qui rende les fonctions fi monotones
(a < b=> f(a) < f(b)).
Ceci est toujours possible (il suffit de mettre l'ordre nul sur A).
Le but est de trouver un ordre qui admet un petit nombre d'elements extremaux.
Ce probleme a des implications tres grandes pour les simulations
a evenements discrets dans lesquelles seuls les etats extremaux doivent etre consideres comme etats initiaux possibles quand les fonctions de changement d'etat sont monotones.
URL sujet détaillé :
:
Remarques : co-encadre par Jean-Marc Vincent
|
|
|
|
|
|
SL307-59 Calculabilité
|
|
|
Description
|
|
Calculabilité : des modèles de calcul à la calculabilité généralisée en passant par l'étude expérimentale.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Julien PROVILLARD : SL307-60 Foulards et automates cellulaires élémentaires
|
|
|
Description
|
|
Lorsqu\'on observe les orbites d\'un automate cellulaire, on retrouve parfois des morceaux d\'orbite d\'un premier dans l\'orbite d\'un second. Cette observation a conduit à plusieurs classifications des automates cellulaires en fonction de leur table de transition, et à définir plusieurs façons de les amalgamer. L\'objet de ce stage est d\'aborder ces notions, de montrer leur pertinence à l\'aide d\'exemples, et éventuellement de les éclairer en termes de catégories.
URL sujet détaillé :
:
Remarques : Co-encadré par Jacques Mazoyer
|
|
|
|
|
|
SL307-61 Interface générique de bas niveau pour réseaux rapides
|
|
|
Description
|
|
Les travaux de l'équipe Runtime (projet commun entre l'INRIA et le LaBRI) dans le domaine du calcul intensif ont notamment conduit à l'élaboration d'une interface de communication multi-protocoles (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, Quadrics, etc.)
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 des heuristiques qui prennent en compte des informations telles que les caractéristiques du réseau sous-jacent ou la taille et les contraintes sémantiques de chacun des segments traités depuis le début d'un message, ainsi que des éléments circonstanciels tels que des opportunités transitoires d'agrégation multi-flot de paquets de données.
La qualité des optimisations dépend en outre fortement de la précision de pilotage offerte par l'interface des pilotes réseaux. Or, l'interfaçage actuel de Madeleine avec les réseaux ne permet pas d'exploiter des fonctionnalités étendues telles que les capacités de filtrages des réseaux Myrinet/MX ou Quadrics/Elan ou prendre en charge l'initialisation appropriée du matériel sur des plateformes à mémoire non uniforme (NUMA). L'objectif de ce stage est donc d'analyser de façon approfondie les besoins de Madeleine d'interfaçage réseau en termes de fonctionnalités et d'expressivité au regard des diverses technologies réseau existantes. Il s'agira alors de faire évoluer le code existant en conséquence, et de vérifier la pertinence et l'effectivité de cette évolution sur des exemples concrêts.
URL sujet détaillé :
:
Remarques : Brice Goglin (brice.goglin.fr)
|
|
|
|
|
|
SL307-62 techniques symboliques de génération d'invariants
|
|
|
Description
|
|
De nombreux systèmes sont spécifiés à l'aide de langages synchrones, comme un réseau de "portes" ou de "filtres". Ces langages sont ensuite typiquement compilés vers du C. Pour obtenir des résultats sur ces systèmes (par exemple: borner certaines variables), on peut analyser le code C résultant; c'est ce que fait le système Astrée.
(http://www.astree.ens.fr)
Il serait cependant peut-être plus avantageux de dégager automatiquement des invariants, de façon modulaires : par exemple, obtenir automatiquement un lien entre les bornes des variables d'entrée d'un module et celles sur les variables de sortie, éventuellement en décomposant le système en sous-modules qu'on analysera séparément. Pour obtenir ces bornes, on utilisera des techniques symboliques et numériques, par exemple des techniques d'élimination des quantificateurs.
Connaissances demandées:
* connaissances de C
* savoir programmer en Caml
* savoir faire des analyseurs syntaxiques
* élements de logique du premier ordre
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
Tarik KACED : SL307-63 Vote électronique
|
|
|
Description
|
|
Ce stage s'intéressera aux protocoles de votes électronique, fondés sur l'utilisation de trois types de primitives cryptographiques. Pour chacune de ces primitives, nous proposons un stage, consistant à étudier les protocoles basés sur cette primitive. Le stage comportera travail bibliographique, étude théorique et implantation, dans des proportions à négocier.
URL sujet détaillé : http://www-verimag.imag.fr/~courant/stages/sujetL3.html
Remarques : L'encadrement pourra avoir partiellement lieu à Lyon.
|
|
|
|
|
|
Chantal KELLER : SL307-64 Manipulation pseudo-haptique d'entités 2D
|
|
|
Description
|
|
*Contexte*
Le sujet de stage proposé concerne la conception et l\'implémentation de métaphores de retour pseudo-haptique pour la manipulation d\'entités sur table magique.
Le retour pseudo-haptique consiste à renvoyer des sensations haptiques (raideur,...) à un utilisateur sans système haptique actif, par un couplage d\'un retour visuel et d\'un capteur de force.
La table magique est un grand écran tactile horizontal.
*Sujet de stage*
L\'équipe i3D mène des recherches sur le retour pseudo haptique depuis plusieurs années. Elle souhaite aujourd\'hui étudier son application dans un contexte nouveau, celui de la manipulation d\'entitées 2D (documents, pions,...) sur table magique.
Le retour pseudo-haptique sera employé soit
- pour faire ressentir à l\'utilisateur une notion de \"poids\" associée à l\'entitée à déplacer,
- soit pour lui faire ressentir une notion de frottement de l\'entitée déplacée sur la table.
La stagiaire participera à la conception et développera une nouvelle métaphore d\'interaction pseudo-haptique associée à la table magique. Une petite application permettant de démontrer l\'effet produit sera ensuite proposée.
*Encadrant *
Sabine Coquillart
Directeur de recherches
INRIA Rhône-Alpes
URL sujet détaillé :
:
Remarques : Réalisation en collaboration avec l\'équipe IIHM du LIG.
|
|
|
|
|
|
Olivier SCHWANDER : SL307-65 Identification de visages
|
|
|
Description
|
|
L'équipe LEAR de l'INRIA http://lear.inrialpes.fr/) étudie de nombreux problèmes liés à l'apprentissage machine pourla reconnaissance visuelle d'objets. Nous travaillons sur des thèmes de catégorisation d'image ("cette image contient-elle un vélo?"), la localisation ("où est le vélo dans cette image?"), l'identification ("est-ce le vélo de Paul?"), et bien d'autres.
Le stage proposé s'inscrit dans une problématique d'identification de visage: il s'agit par exemple de retrouver automatiquement toutes les photos où Paul apparait dans ses photos personnelles. Pour cela, il faudra adapter aux visages les algorithmes que nous utilisons déjà, puis faire une étude comparative avec d'autres algorithmes. C'est une bonne opportunité de découvrir le domaine de la vision par ordinateur.
Le stage se déroulera dans les locaux de
l'INRIA à Montbonnot (www.inrialpes.fr). Il requiert une bonne maitrise du C++, de la rigueur dans les expérimentations, et ne nécessite aucune connaissance en vision par ordinateur. Contacter
URL sujet détaillé :
:
Remarques : Eric Nowak
eric.nowak.fr
|
|
|
|
|
|
Fabien BENUREAU : SL307-66 Applications Web distribuées en Objective Caml
|
|
|
Description
|
|
De plus en plus, un site Web est vu comme une application à part entière, s'exécutant entre un client (le navigateur) et un serveur Web. La programmation de sites dynamiques fait actuellement intervenir différents langages et concepts, parfois peu adaptés aux nouvelles exigences.
La programmation fonctionnelle semble un moyen très propre de résoudre les problèmes d'interaction Web. Ocsigen est un outil de développement Web en Objective Caml basé sur cette idée. Il permet d'implémenter rapidement des sites Web très dynamiques de façon concise, modulaire et sûre, en respectant les standards et usages.
Le but du stage est d'étudier quelques possibilités d'extensions d'Ocsigen pour rendre les sites plus dynamiques en rendant possible l'exécution d'une partie des calculs côté client.
Nous explorerons notamment les possibilités d'écrire le site tout en entier en Objective Caml et les les solutions qui s'offrent à nous pour exécuter certaines partie sur un navigateur. L'accent sera mis sur l'intégration de ces possibilités avec les concepts utilisés par Ocsigen pour décrire l'interaction Web.
URL sujet détaillé : http://www.pps.jussieu.fr/~balat/stagelyon.php
Remarques : possibilité de rémunération à discuter
|
|
|
|
|
|
Nicolas ESTIBAL : SL307-67 Génération de code GPU pour un langage intermédiaire data parallel
|
|
|
Description
|
|
L'objectif de ce stage est de mettre en óuvre un générateur de code pour carte graphique ATI à partir d'un langage intermédiaire data parallel. Ce langage se présente en format XML et il s'agira de produire du code CTM (Close To Machine) permettant de programmer les cartes graphiques ATI de dernière génération.
Le travail comportera les étapes suivantes:
- analyse de la documentation de CTM
- mise en oeuvre d'un parser XML du langage intermédiaire data parallel
- mise en oeuvre de la génération de code
- tests sur des noyaux de calcul numérique
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SL307-68 Problèmes de jeux quantitatifs
|
|
|
Description
|
|
Les systèmes multi-agents sont des systèmes de transitions dont l'évolution est soumise aux actions simultanées de plusieurs agents : à chaque étape, les agents choisissent l'action qu'ils souhaitent faire, et la transition correspondant à l'ensemble de ces choix est appliquée. Dans le domaine de la vérification de systèmes informatiques, ces systèmes permettent de modéliser des problèmes de contrôle, et d'appliquer des techniques de model-checking pour vérifier la contrôlabilité d'un système.
Ces modèles ont récemment été étendus pour inclure également des informations quantitatives sur le système modélisé (par exemple, sur le temps nécessaire pour effectuer une transition, sur le gain des différents joueurs dans certains états, ...).
Ces aspects quantitatifs sont praticulièrement intéressants en théorie des jeux, mais ont été encore assez peu étudiés dans le cadre de l'informatique théorique. Plusieurs questions peuvent être abordées :
-=AD Comment calculer les équilibres de Nash dans ces jeux pour des problèmes d'accessibilité ? Quelle est la complexité de ce problème ?
-=AD Si le gain global est réparti équitablement entre les joueurs d'une coalition, comment calculer la coalition optimale permettant de maximiser le gain dans un tel jeux ?
- les algorithmes de vérification de la logique ATL ont été étendus récemment pour inclure des contraintes quantitatives. Ces algorithmes reposent cependant sur le fait que tous les coûts des transitions sont strictement positifs. Qu'en est-il lorsque les coûts peuvent être nuls ?
URL sujet détaillé :
:
Remarques : Co-encadrant : Thomas Brihaye
http://www.lsv.ens-cachan.fr/~brihaye/
|
|
|
|
|
|