S   t a g e s   d e   M 1
  Stages M1  
  Soumission  
  Sujets  
  Planning  

Stages proposés 66 sujets à ce jour  

SM110-78 sujet vide  
Encadrement  
Encadrant : Alexandre MIQUEL(écrire)
Labo/Organisme : LIP
Ville : LYON

Description  
(sujet vide)


SM110-79 Analyse géométrique de microstructures de neige 3D  
Encadrement  
Encadrant : David COEURJOLLY(écrire)
Labo/Organisme : LIRIS
Ville : Villeurbanne

Description  
*This subject is related to the ANR Grant "DigitalSnow" (PhD Grants available)

* L'objectif du projet et d'avoir une meilleure compréhension des modèles physiques qui régissent les structures neigeuses afin de simuler numériquement des déformations de microstructures de neige (et à plus large échelle de construire des modèles d'avalanche pertinents). En collaboration avec le centre d'étude de la neige de MeteoFrance, nous disposons d'images 3D de haute résolution 600x600x600 de microstructures sur lesquelles nous souhaitons développer des outils d'analyse géométrique (courbures, aire de surface, compacité ...).

L'objectif du stage sera donc, d'un point de vue théorique de reprendre la littérature sur les estimateurs différentiels discrets, et de s'intéresser à des notions de convergence asymptotique. D'un point de vue expérimental, il s'agira d'implémenter certains de ces estimateurs dans une bibliothèque opensource en construction(http://liris.cnrs.fr/dgtal) en ayant en tête le fait que les images en entrée sont de très haute résolution (donc problèmes de performances à gérer).

Remarques:
Possibilité de rémunération dans le cadre du projet ANR "DigitalSnow"


SM110-80 Analyse et caractérisation d'objets 3D par applications conformes et géométrie hyperbolique  
Encadrement  
Encadrant : David COEURJOLLY(écrire)
Labo/Organisme : LIRIS
Ville : Villeurbanne

Description  
La caractérisation géométrique de formes 3D a de nos jours des répercutions pratiques très importantes. Il s'agit par exemple d'être capable de mesurer de manière quantitative la différence géométrique entre deux maillages afin de les distinguer. Dans ce contexte, nous nous intéressons à la notion d'application conforme entre deux maillages qui permet une association "naturelle" entre les éléments du premier maillage sur le second (préservant certaines propriétés). L'étape suivante est donc de définir une distance entre les deux structures en exploitant cette application conforme. Une difficulté principale réside dans le fait que dans le cas général (formes avec tunnels ou trous), une telle application est difficile à construire. Une solution à ce problème est de changer le modèle géométrique vers un modèle de géométrie hyperbolique rendant le problème plus simple.

L'objectif du stage sera de poursuivre les développements réalisés autour de ce projet. Le contexte applicatif porte sur une collaboration entre le laboratoire et l'University of California, Davis, USA.

Remarques:
Possibilité de rémunération.


SM110-81 Diagrammes d'épaisseur et analyse de formes 3D  
Encadrement  
Encadrant : David COEURJOLLY(écrire)
Labo/Organisme : LIRIS
Ville : Villeurbanne

Description  
Au cours de précédents développements, nous avons mis en avant l'intérêt du diagramme d'épaisseur pour l'analyse de formes géométriques 2D et 3D. Pour faire simple, le diagramme d'épaisseur associe à chaque point à l'intérieur d'une forme, le rayon de la plus grosse boule contenant ce point, boule elle-même contenue dans la forme. Cette structure est clairement reliée à la notion de squelette ou axe médian de formes. A partir de ce diagramme, de nombreux descripteurs de formes peuvent être définis pour caractériser des objets discrets et maillages. Que ce soit sur des objets discrets (région dans une image) ou de nuages de points, nous avons obtenus plusieurs résultats théoriques sur la complexité de ce diagramme d'épaisseur et sur des algorithmes rapides de calcul.

L'objectif du stage sera de poursuivre les travaux sur ce problème en se focalisant sur une implémentation 3D via la bibliothèque de géométrie algorithmique CGAL.

Remarques:
Co-encadrement avec Raphaelle Chaine (LIRIS-geomod)


SM110-82 Bilan radiatif d\'un échantillon de neige  
Encadrement  
Encadrant : David COEURJOLLY(écrire)
Labo/Organisme : LIRIS
Ville : Villeurbanne

Description  
L\'objectif à long terme du projet ANR DigitalSnow est d\'étudier le comportement de la neige en fonction de son état (fraiche, tassée, gélée, ventée, etc) en se basant sur des analyse géométriques d\'images 3D de microstructure de neige. A partir de ces analyse à très petites échelles, l\'étape suivante est de fournir des modèles numériques simulant l\'évolution d\'un manteau neigeux selon des contraintes thermiques (réchauffement) ou mécaniques (tassement,...).
L\'objectif de ce stage est de fournir un outil d\'étude aux glaciologues pour un état particulier de la neige : permettre de déterminer comment la neige absorbe et réfléchit l\'énergie quelle reçoit du soleil tout au long de la journée pour ensuite permettre de prédire l\'évolution de son état en intégrant cette information énergétique dans des équations d\'évolution physiques. La simulation à mettre en place est une application directe du \"photon mapping\", technique issue de la synthèse d\'image.
Le stage sera composé de phases d\'implémentation et de tests dans un environnement logiciel existant mais également d\'une partie plus exploratoire sur des techniques de simulations spécialisées a priori mieux adaptées à ce cas. Une comparaison avec une méthode réference est également envisagée.

mots clés: photon mapping, scan, voxels, lancer de rayons, monte carlo, simulation, cristaux, neige.

Remarques:
Co-encadrement avec Jean-Claude Iehl (LIRIS-R3AM)


SM110-83 Compilation de circuits sécurisés pour la cryptographie sur les courbes elliptiques  
Encadrement  
Encadrant : Arnaud TISSERAND(écrire)
Labo/Organisme : IRISA
Ville : LANNION

Description  
Un compilateur de circuits intégrés numériques pour la cryptographie sur les courbes elliptiques (ECC) est développé dans l'équipe CAIRN de l'IRISA. À partir d'une description mathématique des calculs requis pour une application ECC et d'une description de haut niveau de l'architecture du circuit, il produit le code VHDL optimisé d'un (co-)processeur autonome. Il utilise une bibliothèque d'algorithmes arithmétiques et de représentations des nombres et des points de la courbe. Différents objectifs peuvent être spéciés pour orienter les phases de compilation :
- vitesse, débit, latence (niveau de parallélisme interne, pipeline) ;
- taille du circuit (pour le coût silicium) ;
- consommation d'énergie (choix des algorithmes et des représentations) ;
- sécurité par rapport à des attaques physiques.
Le stage portera sur la sécurisation du processeur face à certaines attaques par canaux cachés en analyse de la consommation d'énergie. Ces attaques utilisent la corrélation entre le secret (valeur des bits de la clé) et l'activité
électrique du circuit (transitions des données ou parasites). Deux pistes sont envisageables : rendre l'activité du circuit indépendante du secret (courbes particulières, randomisation) ou bien limiter les variations d'activité (équilibrage des calculs, codages physiques spécifiques). Notre approche se situera au niveau des algorithmes arithmétiques et des représentations des données (aux niveaux du corps fini et de la courbe utilisés) et puis de leur codage physique
dans le circuit. En particulier, les compromis entre la taille des opérateurs et le nombre d'unités de calcul disponibles en parallèle seront étudiés (multiples petites unités contre quelques unités très larges). Les résultats seront analysés expérimentalement en utilisant le banc d'attaques (sondes, oscilloscope numérique rapide et machine de traitement) et des cartes FPGA disponibles dans notre équipe. Les meilleurs algorithmes et représentations seront intégrés au
compilateur.

Accéder au sujet détaillé

Remarques:
Une indemnité de stage sera possible au tarif fixé par l'IRISA.


SM110-85 Un radar pour l'internet  
Encadrement  
Encadrant : Matthieu LATAPY(écrire)
Labo/Organisme : LIP6 - CNRS et UPMC
Ville : Paris

Description  
Lorsqu'on est sur une machine de l'Internet (une source), il est possible de connaitre le chemin suivi par les informations partant de cette machine vers n'importe quelle autre machine de l'Internet (une destination). Cette approche est largement utilisée pour explorer la topologie de l'Internet (machines et liens entre elles).

Nous proposons ici un nouveau point de vue : nous allons voir l'exécution de traceroute comme une sonde qui, utilisée périodiquement, va nous permettre de construire un radar pour l'Internet.


Accéder au sujet détaillé


SM110-87 Dynamiques de graphes  
Encadrement  
Encadrant : Matthieu LATAPY(écrire)
Labo/Organisme : LIP6 - CNRS et UPMC
Ville : Paris

Description  
L\'étude des grands graphes apparaissant en pratique a connu ces dernières années un essor
hors du commun. Les objets étudiés sont d\'origines diverses, comme par exemple la topologie de l\'internet (machines et câbles), les graphes du web (pages et liens), les échanges pair-à-pair (qui échange des données avec qui), mais aussi les réseaux sociaux, les réseaux biologiques ou les réseaux linguistiques.

La plupart de ces graphes ne sont pas fixes. Au contraire, ils évoluent au cours du temps : des sommets et/ou des arêtes apparaissent et disparaissent. Cette dynamique joue un rôle essentiel dans de nombreux cas. Par exemple, la dynamique du web peut permettre d\'identifier des thèmes émergents, celle des échanges permet d\'étudier les comportements des utilisateurs (et d\'utiliser ces résultats pour optimiser les protocoles), la dynamique de l\'internet permet d\'étudier sa fiabilité, etc.

Or, il est en général délicat de capturer ces dynamiques et, même lorsque des données sont disponibles, il est non-trivial de les décrire et de les analyser. Cette problématique, bien qu\'identifiée comme essentielle, reste donc encore aujourd\'hui largement à défricher. Le but de ce stage sera d\'explorer quelques idées
+émergentes pour ce faire, sur la base de cas concrets.


Accéder au sujet détaillé


SM110-88 Modélisation des graphes de terrain  
Encadrement  
Encadrant : Matthieu LATAPY(écrire)
Labo/Organisme : LIP6 - CNRS et UPMC
Ville : Paris

Description  
Dans de très nombreux contextes applicatifs, on rencontre de grands graphes n\\\'ayant aucune structure simple apparente, que nous appellerons graphes de terrain (par opposition aux graphes
explicitement contstruits par un modèle ou une théorie). Citons par exemple la topologie de l\'internet (routeurs et câbles entre eux), les graphes du web (pages web et liens hypertexte entre elles), les échanges divers (pair-à-pair, e-mail, etc), mais aussi les réseaux sociaux, biologiques ou linquistiques.

Il est apparu récemment que la plupart de ces grands graphes ont des propriétés statistiques en commun, et que ces propriétés les différencient fortement des graphes aléatoires utilisés jusqu\'alors pour les modéliser. Depuis, une intense activité a été développée pour proposer des modèles plus adapté.

L\'état de l\'art reste toutefois largement insuffisant. Nous proposons dans ce stage d\'explorer deux nouvelles voies particulièrement prometteuses (voir le pdf).


Accéder au sujet détaillé


SM110-89 Structure Multi-échelles des Grands Graphes  
Encadrement  
Encadrant : Matthieu LATAPY(écrire)
Labo/Organisme : LIP6 - CNRS et UPMC
Ville : Paris

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.


Accéder au sujet détaillé


SM110-90 Décompilation pour l'analyse de programmes au niveau binaire  
Encadrement  
Encadrant : Sébastien BARDIN(écrire)
Labo/Organisme : CEA LIST
Ville : Saclay (région parisienne)

Description  
L'analyse statique de programmes vise, à partir d'une description du programme,
à inférer automatiquement des propriétés vérifiées par celui-ci [1].
Les techniques standards d'analyse statique travaillent à partir du code source du logiciel,
écrit par exemple en C ou Java. Cependant l'analyse statique de programmes à partir de leur code exécutable
connaît un regain d'intérêt, motivé par les applications potentielles en sécurité et sûreté [2].

Le thème du stage est la décompilation de codes exécutables en programmes de plus haut niveau pour pouvoir
réutiliser les techniques existantes de vérification de programmes. Le stagiaire devra concevoir une
approche de décompilation sûre en s'appuyant sur les méthodes d'analyse statique de programmes [1]
et les résultats déjà obtenus au CEA [2] en termes de reconstruction du Graphe de Flot de Contrôle. Alors
qu'une retranscription directe d'un modèle bas niveau en code C d'aussi bas niveau est assez aisée, un point important
sera d'identifier quelles informations utiles à l'analyse peuvent être retrouvées au niveau du code exécutable.
Des points difficiles attendus sont par exemple de retrouver les fonctions du programme, et de limiter au maximal
l'utilisation de la mémoire globale en retrouvant les variables locales.
Le stagiaire devra ensuite valider son approche en implantant un prototype (OCaml)
et en évaluant sur des cas concrets la chaine de vérification obtenue. Le code C synthétisé
pourra être analysé par exemple avec le logiciel Frama-C (http://frama-c.com/).
Les travaux de Chaki et Ivers [3] seront un point de départ intéressant.


Références

[1] Bardin, S., Herrmann, P., Védrine, F. : Refinement-based CFG Reconstruction from
Unstructured Programs. In : VMCAI 2011. Springer (2011)
[2] Chaki, S., Ivers, J. : Software model checking without source code. In : ISSE, vol. 6 (3),
2010
[3] Nielson, F., Nielson, H. R, Hankin, C. : Principles of Program Analysis. Springer, 1999.



Accéder au sujet détaillé

Remarques:
rémunération : oui + aide au logement pour les non parisiens

le stage est co-encadré par Franck Védrine


SM110-91 Decomposition of Stochastic Systems modeling Biological Pathways  
Encadrement  
Encadrant : Blaise GENEST(écrire)
Labo/Organisme : CNRS, UMI IPAL, Singapour
Ville : Singapour

Description  
Building and Validating Biological Pathways is a corner stone in understanding cells behavior.
There are many ways to model biological Pathways (Differential equations…). One of them is through Dynamic Bayesian Networks (DBNs for short): A DBN models local interactions between nodes (in biological pathways, each node represents a molecular species). Each node –viewed as a random variable- can take different values (here: concentration level intervals). The DBN specifies for each node X which “parent” nodes influences its next state (the parent nodes will consist of the molecules taking part in the reactions that produce and consume the molecular species associated with the node X). The quantitative and stochastic nature of this influence is given as a conditional probability tables; the probability of the next state of X taking a given value according to the state of its predecessors. The basic inferencing task in a DBN is to compute the probability of each node taking a given value. However, such inference cannot be performed exactly for large DBNs. One needs approximate methods. See: http://perso.crans.org/~genest/PALGT11.pdf.

The current inference procedures either produce high error margin or require an excessive computational effort. We propose to address this by decomposing the DBN. Several procedures can be used to do so. First, one can assume that all nodes are independent, as done by the Factored Frontier inference procedure. Then, one can evaluate which nodes are stable and which ones are not stable. Then the non stable nodes can be decomposed into sets of components. Assuming the values of the stable nodes to be as computed first, the non stable nodes can be computed inductively with a more precise method. In the likely case where the stable nodes keeps the same value (which should be the case as they have been evaluated stable at the beginning), we would be done. Else, the network is decomposed into finer pieces before iterating the procedure.

Requested job:
Definition and Implementation of a decomposition strategy.
Validation on DBNs that we already built from biopathways.
Proposal for improvements.


Accéder au sujet détaillé

Remarques:
Le stage aura lieu a Singapour. Une gratification de stage sera donné au stagiaire.


SM110-92 Formal proof of decision procedures for the combinations of equational theorieside  
Encadrement  
Encadrant : Frederic BLANQUI(écrire)
Labo/Organisme : INRIA
Ville : Beijing (China) or Rocquencourt (France)

Description  
General overview of the domain: Many algorithms use data structures with particular invariants (e.g. a sorted list of values, a list of values with no repetition, etc.) and, to ensure that the invariants are always satisfied, one generally uses abstract or private data types with construction functions. Interestingly, many invariants can be described by algebraic equational theories: sorting corresponds to commutativity, the absence of repetition to idempotence, etc. Moca (moca.inria.fr) is a generator of construction functions for such data types in the OCaml functional programming language.

Goal of the project: The goal of the project is to formally prove in the proof assistant Coq that the construction functions generated by Moca are correct. The first task is to study the various possible representations in Coq of the OCaml functions generated by Moca. Indeed, because of Coq\'s restrictions on the definition of functions, especially for termination, the construction functions generated by Moca may not definable in Coq as they can be in OCaml. Then, he will prove the correctness of the construction functions for some particular equational theories on a fixed signature (e.g. the theory of (commutative) monoids and the theory of (commutative) groups). He will then try to develop a framework and tactics in Coq so that these proofs can be done automatically and in a modular way, that is, by combining tactics for each elementary equational theory (associativity, commutativity, etc.). Finally, if time permits, he will extend Moca itself so that, together with the OCaml construction functions, it generates a Coq proof of their correctness.


Accéder au sujet détaillé

Remarques:
Co-supervisor: Pierre Weis (http://bat8.inria.fr/~weis/). The internship can take place either at Beijing (China) or at Rocquencourt (France).

Frederic Blanqui is an INRIA researcher in the FORMES team. The FORMES team is an INRIA-CNRS-Tsinghua University team of the LIAMA French-Chinese Consortium. The FORMES team is located at Tsinghua University, Beijing, China.

Pierre Weis is an INRIA researcher in the ESTIME team located at INRIA Rocquencourt, France.


SM110-93 Lissage de nuages de points respectant les arêtes vives  
Encadrement  
Encadrant : Quentin MÉRIGOT(écrire)
Labo/Organisme : LJK / Université Grenoble I
Ville : Grenoble

Description  
Il s’agit d'étudier certains aspects de la reconstruction de surfaces lisses par morceaux à partir de données discrètes (nuages de points). On se restreindra aux surfaces qui bordent un compact de portée positive. La portée est une notion quantitative de régularité «extrinsèque», particulièrement bien adaptée aux questions d'inférence géométrique et de reconstruction.

Nous considérons donc un nuage de points qui approche un compact de portée positive connue. Le but est de reconstruire un nuage de points lissé ́échantillonnant la surface bordant ce compact, muni de normales, et où l’on aura identifié et bien échantillonné le lieu des arêtes vives. A partir de ces informations, il est envisageable de reconstruire la surface en utilisant des algorithmes existants.

Le stagiaire sera amené à étudier plusieurs approches pour résoudre ce problème, qu'il pourra valider expérimentalement (en utilisant la bibliothèque C++ CGAL) et/ou théoriquement.


Accéder au sujet détaillé

Remarques:
Co-encadrement avec Boris Thibert. Gratification de 400€/mois possible.


SM110-94 Factorisations 1-recouvrantes et leurs multiples interprétations  
Encadrement  
Encadrant : Arnaud PÊCHER(écrire)
Labo/Organisme : LaBRI / Université Bordeaux 1
Ville : Bordeaux

Description  
L'article "Thin Lehman matrices arising from finite groups" de Shinohara établit de multiples connexions entre divers domaines des mathématiques discrètes: théorie des graphes (graphes partitionnables), théorie des groupes finis (factorisations 1-recouvrante), algèbre (matrices de Lehman), théorie des nombres (systèmes de nombres de De Bruijn) ...

L'objet de ce projet est dans un premier temps de comprendre et approfondir ces connexions en se focalisant sur le cas des groupes cycliques (le plus simple et le plus étudié). Dans un second temps, le cas des groupes non-commutatifs avec un petit nombre d'éléments sera étudié.

Pour mener à bien cette étude, il sera utile de réaliser quelques développements logiciels faciles:
* génération des systèmes de nombre de De Bruijn;
* procédure testant si deux parties $A$ et $B$ d'un groupe $G$ forme une factorisation 1-recouvrante de $G$;
* procédure permettant de "symétriser" (cf Théorème 1.6) une factorisation 1-recouvrante d'un groupe commutatif;
* procédure permettant de déterminer si un groupe fini possède des factorisations 1-recouvrante.


Article associé: Shinohara, "Thin Lehman matrices arising from finite groups", Linear Algebra and its Applications, à paraître


SM110-95 Analyse et conception d'un système de vote  
Encadrement  
Encadrant : Véronique CORTIER(écrire)
Labo/Organisme : LORIA
Ville : Nancy

Description  
Plusieurs types de systèmes de vote permettent de voter à distance. Un système classique de vote par correspondance consiste à glisser son bulletin dans une première enveloppe puis mettre celle-ci dans une 2e, que l'on signe et que l'on expédie. De tels systèmes supposent une confiance totale dans l'entité chargée de la collecte et du comptage des votes. Une variété d'autres systèmes ont été développés, en introduisant par exemple des codes à barres pour faciliter le dépouillement. Cependant, des travaux récents ont montré que ces systèmes pouvaient être sujet à des attaques, comme un bourage d'urne massif.

Plus récemment, des protocoles totalement dématérialisés ont été proposés.
Les protocoles de votes électroniques permettent ainsi de réaliser des élections à distance (depuis son ordinateur), tout en préservant, en théorie, les bonnes propriétés d'un vote standard (confidentialité des votes, fiabilité et vérifiabilité du résultat, résistance à la coercition).

L'objectif de ce stage sera de concevoir un protocole de vote hybride, utilisant le papier et la Poste pour faciliter le vote (nul besoin d'un ordinateur) mais utilsant la cryptographie pour assurer de meilleure garanties de sécurité. On pourra en particulier d'inspirer des techniques développés dans le cadre du vote électronique.

Dans un deuxième temps et si le temps le permet, l'objectif sera de proposer une formalisation de ce protocole, ainsi que la preuve des propriétés de sécurité les plus standards, dans un cadre formel. Nous étudierons en priorité la confidentialité des votes, la vérification de l'éligibilité et la possibilité de vérifier la prise en compte des votes (individuelle et universelle). Il est bien sûr possible que des failles soient détectées à ce stade, auquel cas des modifications seront proposées.
Selon les compétences et les goûts de l'étudiant, nous pourrons nous orienter plutôt vers des preuves de sécurité dans des modèles cryptographiques ou des preuves dans des modèles symboliques, utilisant plutôt des compétences en logique.

Remarques:
Ce stage pourra être indemnisé. En particulier, ce stage a le support de la bourse Européenne ProSecure (ERC Starting Grant).


SM110-96 Procédure de décision pour la sécurité des protocoles cryptographiques  
Encadrement  
Encadrant : Véronique CORTIER(écrire)
Labo/Organisme : LORIA
Ville : Nancy

Description  
Les protocoles cryptographiques visent à sécuriser les communications sur des réseaux ouverts comme Internet. À l'aide de primitives cryptographiques, ils permettent de d'assurer par exemple la confidentialité des échanges ou l'authentification des utilisateurs, si nécessaire.
Une faille de conception pouvant permettre des attaques à grande échelle, il s’agit d’un type d’applications pour lequel une analyse
formelle et une preuve de sécurité sont particulièrement indiquées.

De nombreux travaux ont permis de développer des modèles abstraits relativement simples pour les protocoles, utilisant par exemple des clauses de Horn ou des algèbres de processus.
Dans ce cadre, des outils permettent d'analyser automatiquement la sécurité des protocoles. Cependant, tester une propriété aussi simple que la confidentialité d'une donnée est un problème indécidable, si on considère un nombre non borné de sessions (i.e. un nombre arbitraire d'exécutions du protocole).
Par contre, cette même propriété redevient décidable (NP-complet) si on se limite à un nombre fixe de sessions.

Même si tester la confidentialité est indécidable en théorie, les protocoles utilisés en pratique vérifient la propriété suivante : s'il existe une attaque, alors il existe une attaque n'impliquant qu'une ou deux sessions du protocole. Cette propriété est bien sûr fausse en général.

L'objectif de ce stage est d'explorer dans quelle mesure il est possible de montrer cette propriété pour une classe importante de protocoles, capturant la plupart des protocoles proposés en pratique. Des travaux relativement récents semblent en effet aller dans ce sens.


Remarques:
Ce stage pourra être indemnisé. En particulier, ce stage a le support de la bourse Européenne ProSecure (ERC Starting Grant).


SM110-97 Analyse formelle de la connaissance d'un attaquant pour les protocoles cryptographiques  
Encadrement  
Encadrant : Véronique CORTIER(écrire)
Labo/Organisme : LORIA
Ville : Nancy

Description  
Les protocoles cryptographiques visent à sécuriser les communications sur des réseaux ouverts comme Internet. À l'aide de primitives cryptographiques, ils permettent de d'assurer par exemple la confidentialité des échanges ou l'authentification des utilisateurs, si nécessaire.
Une faille de conception pouvant permettre des attaques à grande échelle, il s’agit d’un type d’applications pour lequel une analyse
formelle et une preuve de sécurité sont particulièrement indiquées.

De nombreux travaux ont permis de développer des modèles abstraits relativement simples pour les protocoles, utilisant par exemple des clauses de Horn ou des algèbres de processus.
A la base de tous ces modèles se trouvent les termes (qui peuvent être vus comme des graphes étiquetés) qui servent à représenter les messages échangés et leurs structures cryptographiques.
Un problème de base consiste donc à se demander quels sont les termes déductibles (i.e. calculables par un attaquant), à partir d'un ensemble (fini) de termes donnés (par exemple ceux interceptés par l'attaquant). La notion de déduction est cependant trop faible dans de nombreux cas, notament lorsqu'on étudie les protocoles de vote électronique. La question n'est alors plus de savoir si un intrus peut connaître les valeurs des vote 0 ou 1 (valeurs qu'il connait toujours) mais de savoir s'il peut distinguer une exécution où un participant vote 1 d'une exécution où il vote 0.

L'objectif de ce stage est d'explorer d'explorer la décidabilité de l'équivalence de séquences de messages (appelée équivalence statique) en présence d'une fonction longueur qui révèle la taille d'un terme. Cela reflète le fait qu'un attaquant peut observer la longueur d'un message, ce qui est une source d'information potentielle.
Ce stage fera appel à des résultats de logique, réécriture et potentiellemnt un peu d'algèbre.


Remarques:
Ce stage pourra être indemnisé. En particulier, ce stage a le support de la bourse Européenne ProSecure (ERC Starting Grant).


SM110-98 Utude théorique des propriétés spectrales des systèmes d’échantillonnage stochastiques  
Encadrement  
Encadrant : Victor OSTROMOUKHOV(écrire)
Labo/Organisme : LIRIS UMR 5205/CNRS
Ville : Lyon

Description  
La théorie d’échantillonnage joue un rôle prépondérant dans la synthèse d’image. Les systèmes d’échantillonnage multidimensionnels évolués avec des qualités spectrales contrôlables peuvent également trouver leur application dans d’autres domaines qui font appel aux méthodes de Monte-Carlo et de Quasi Monte-Carlo multidimensionnelles, par exemple, dans des systèmes de simulations.

Dans ce travail de stage, nous proposons d’étudier sur le plan théorique les propriétés spectrales des systèmes d’échantillonnage stochastiques connus. L’étude commencera par les deux cas les plus simples et les plus utilisés : l’échantillonnage stratifié et l’échantillonnage à l’aide des disques de Poisson. L’étude de cas plus évolués en découlera.


Remarques:
possibilité de rénumération
possibilité de publication
possibilité de poursuite au niveau doctoral


SM110-99 Approche spectrale appliquée aux symétries engendrées par transformations d’auto ressemblance  
Encadrement  
Encadrant : Victor OSTROMOUKHOV(écrire)
Labo/Organisme : LIRIS UMR 5205/CNRS
Ville : Lyon

Description  
La symétrie joue un rôle important dans notre vie, en fournissant à notre cerveau une représentation compacte des réalités complexes du monde extérieur. C’est pour cette raison que le traitement des symétries est une branche très active dans la vision par ordinateurs, dans le traitement et la synthèse d’images. Les travaux très récents ont permis de caractériser les symétries le plus répandues (symétrie bilatérale, symétrie rotationnelle ou miroir) grâce à l’étude spectrale des matrices dites matrices de correspondance symétrique. Dans ce travail de stage, nous proposons d’étudier la possibilité d’appliquer l’étude spectrale aux symétries d’un type plus évolué : celles engendrées par une transformation d’auto ressemblance. On trouve ce genre de symétrie partout dans le règnes végétal et animal : dans l’arrangement des branches et des feuilles des plantes, dans les arrangements des feuilles, fleurs et des graines dans les phyl
lotaxies, dans la répartition des chambres des mollusques, etc.
Ce travail de stage demandera à un étudiant de faire preuve d’imagination et de connaissances mathématiques considérables ainsi que de maîtriser des outils de l’analyse spectrale : calcul matriciel évolué, étude des valeurs propres pour les matrices éparses de grande dimension, etc.


Remarques:
possibilité de rénumération
possibilité de publication
possibilité de poursuite au niveau doctoral


SM110-100 Etude des propriétés spectrales des empilements compacts à plusieurs sphères.  
Encadrement  
Encadrant : Victor OSTROMOUKHOV(écrire)
Labo/Organisme : LIRIS UMR 5205/CNRS
Ville : Lyon

Description  
La théorie d’échantillonnage joue un rôle prépondérant dans la synthèse d’image. Les systèmes d’échantillonnage multidimensionnels évolués avec des qualités spectrales contrôlables peuvent également trouver leur application dans d’autres domaines qui font appel aux méthodes de Monte-Carlo et de Quasi Monte-Carlo multidimensionnelles, par exemple, dans des systèmes de simulations.
On propose à l’étudiant d’examiner les propriétés spectrales des empilements compacts à plusieurs sphères, ainsi que les méthodes rapides pour générer de tels arrangements en 2D, en 3D, et en dimensions plus élevées. Ce projet est passionnant et très ambitieux. Pour comprendre à quel point le problème des empilements compacts est non-trivial, lisez l’article de Pfender et Ziegler : vous y verrez que certaines réponses aux problèmes posés depuis des siècles ont été apportées en 2003 par un mathématicien peu connu. Ou lisez les livres de Thompson ou de Conway & Sloane, pour voir à quel point le problème des empilements compacts est lié à d’autres branches de la science, par exemple à la théorie des groupes ou bien à la théorie des codes correcteurs.

Références :
Pfender, Florian; Ziegler, Günter M. (September 2004), \"Kissing numbers, sphere packings, and some unexpected proofs\", Notices of the American Mathematical Society: 873–883, http://www.ams.org/notices/200408/fea-pfender.pdf.
Thomas M. Thompson (1983) \"From error-correcting codes through sphere packings to simple groups\".
Conway, J.H. & Sloane, N.J.H. (1998) \"Sphere Packings, Lattices and Groups\".


Remarques:
possibilité de rénumération
possibilité de publication
possibilité de poursuite au niveau doctoral


SM110-101 TOPOLOGIE DES GRAPHES PLONGES Application à la vérification/comparaison du calcul de la topologie de courbes algrébriques planes  
Encadrement  
Encadrant : Marc POUGET(écrire)
Labo/Organisme : INRIA-Nancy, LORIA
Ville : Nancy

Description  
Problématique de recherche:

Le sujet relève du domaine de la théorie topologique des graphes avec
une application à la géométrie algébrique réelle algorithmique.

La motivation de ce sujet est la vérification/comparaison des
résultats de différents programmes permettant le calcul de la
topologie de courbes algébriques planes (par exemples: Isotop
{http://vegas.loria.fr/isotop/}, Exacus
{http://exacus.mpi-inf.mpg.de/cgi-bin/xalci.cgi}). Une courbe
algébrique C est une courbe définie implicitement par un polynôme f
à deux variables: C={ (x,y) in {R}^2, f(x,y)=0}. Le calcul de la
topologie la courbe C consiste à décrire les différentes
composantes connexes et leurs positions relatives dans le plan. Cette
topologie peut être représentée par un graphe plongé dans le plan (par
exemple une ``doubly-connected edge-list''), mais la combinatoire de
ce graphe peut varier selon la méthode employée pour le calcul. Le but
est de comparer la topologie malgré les variantes combinatoires de
tels graphes. En d'autres termes, il s'agit de déterminer
algorithmiquement si deux graphes plongés donnés définissent deux
espaces topologiques homéomorphes relativement au plan (c'est à dire
s'il existe un homéomorphisme du plan transformant l'un en l'autre).

Une approche naturelle pour ce problème de comparaison consiste à
réduire la sortie de chaque programme en une forme ``canonique'' et de
définir un isomorphisme combinatoire qui corresponde à l'équivalence
topologique des plongements. Cette étape de formalisation conduira à
la conception d'un algorithme et son analyse de complexité. Enfin
l'implantation de l'algorithme dans le cadre de la bibliothèque de
géométrie algorithmique CGAL
({http://www.cgal.org}{www.cgal.org}) permettra de résoudre le
problème d'isomorphisme topologique de graphe plongé dans le plan et
sera utilisée pour l'application à la topologie des courbes
algébriques.



Objectifs du stage:

Le candidat devra dans un premier temps faire un travail de
bibliographie dans le domaine des graphes topologiques. Il devra
adapter les méthodes de ce domaine au cas particulier des graphes non
connectés plongées dans le plan et démontrer un théorème d'équivalence
entre plongement combinatoire et topologique. Le deuxième aspect du
sujet est algorithmique: concevoir un algorithme qui transforme un
plongement de graphe en une forme canonique et effectue le test
d'isomorphisme entre formes canoniques. Le dernier aspect est
l'implantation de l'algorithme en C++ dans la bibliothèque CGAL, puis l'utilisation de
cette implantation pour l'application proposée à la topologie des
courbes algébriques.


Accéder au sujet détaillé

Remarques:
Possibilité de rémunération environ 400 euros/mois


SM110-102 Ordonnancement de tâches dont le temps opératoire dépend du temps ou: comment éteindre des incendies le plus rapidement possible  
Encadrement  
Encadrant : Julien MONCEL(écrire)
Labo/Organisme : LAAS-CNRS
Ville : Toulouse

Description  
Il s'agit d'étudier un problème d'ordonnancement, où la durée d'une tâche dépend du moment où celle-ci est réalisée. Une application typique de ce type de modèle est le cas des incendies. Plus on attend, plus ceux-ci s'étendent, et plus il faut du temps pour éteindre ceux-ci. Dans ce cadre, quelle(s) stratégie(s) adopter pour qu'une équipe de pompiers éteigne des incendies le plus vite possible ?

Accéder au sujet détaillé

Remarques:
Le stage est co-encadré par Pierre Lopez, directeur de recherche au CNRS http://homepages.laas.fr/lopez/


SM110-103 Model Transformation  
Encadrement  
Encadrant : Rachid ECHAHED(écrire)
Labo/Organisme : LIG
Ville : Grenoble

Description  
Very high level languages such as modeling languages or declarative programming languages contribute significantly to improving the quality of software (specification, programming, validation). Most of these languages are based on trees (e.g. first-order terms, lambda-terms). This does not give them the ability to easily transform models or structures represented as graphs (see e.g. models from UML). However, there exists in the literature a large number of applications which use data structures or complex models represented as graphs and technically implemented through pointers.

Model transformation is often achieved using rewriting techniques [1,5,6,7,8]. Such techniques are the bases of high-level programming languages as well as software validation methods. We develop in our team new approaches to model/graph transformation [2,3,4]. This is an area rich in research topics that range from theory to applications. The choice of the subject will be in agreement with the student according to its affinities. For example, we mention here two subjects: “techniques of visual programming dedicated to the transformation of models/graphs” or “ new validation techniques in the presence of model/graph transformation systems”. More details are available from the above supervisor (echahed@imag.fr). PhD is possible.

References

[1]F.~Baader and T.~Nipkow. Term rewriting and all that.Cambridge University Press, 1998.

[2] Ph. Balbiani, R.Echahed, A. Herzig: A Dynamic Logic for Termgraph Rewriting. ICGT 2010: 59-74

[3]D. Duval, R. Echahed and F. Prost. Modeling Pointer Redirection as Cyclic Term-graph Rewriting. In Electronic Notes in Theoretical Computer Science Volume 176, Issue 1, 28 May 2007, Pages 65-84.

[4] R. Echahed: Inductively Sequential Term-Graph Rewrite Systems. In Procs of 4th International Conference, ICGT 2008, LNCS 5214. pp 84-98.

[5]H.~Ehrig, G.~Engels, H.-J. Kreowski, and G.~Rozenberg, editors. Handbook of {G}raph {G}rammars and {C}omputing by {G}raph {T}ransformations, {V}olume 2: {A}pplications, {L}anguages and {T}ools}. World Scientific, 1999.

[6]H.~Ehrig, H.-J. Kreowski, U.~Montanari, and G.~Rozenberg, editors.{em Handbook of {G}raph {G}rammars and {C}omputing by {G}raph {T}ransformations, {V}olume 3: {C}oncurrency, {P}arallelism and {D}istribution}. World Scientific, 1999.

[7]G.~Rozenberg, editor.{em Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations}. World Scientific, 1997.

[8]D.~Plump.Term graph rewriting. In H.~Ehrig, G.~Engels, H.~Kreowski, and G.~Rozenberg, editors,Handbook of Graph Grammars and Computing by Graph Transformation}, volume~2. World Scientific, 1998.


Accéder au sujet détaillé

Remarques:
Rémunération possible (Master rt Thèse)


SM110-105 Communautés dans les graphes, parallélisme et bioinformatique  
Encadrement  
Encadrant : Vincent MIELE(écrire)
Labo/Organisme : CNRS - Biométrie et Biologie Evolutive
Ville : Villeurbanne

Description  
La détection de communautés dans les réseaux ou graphes consiste à regrouper des entités ou sommets qui intéragissent fortement ensemble,
par exemple des groupes d'amis dans une classe. Néanmoins, une nouvelle approche proposée dans Nature en 2010 propose de regrouper cette fois-ci les liens en communautés, de sorte que les sommets appartiennent à plusieurs communautés chevauchantes. Ainsi un même individu peut appartenir à une communauté de liens amicaux et une communauté de liens familiaux. Cette stratégie présenterait un grand intérêt pour étudier les réseaux de gènes, connectés selon leur divergence par rapport à un ancètre commun.
Les gènes, composés de segments appelés domaines, pourraient ainsi appartenir à plusieurs communautés représentant leur histoire au cours de l'Evolution darwinienne.

Le but du stage sera d'une part d'étudier la pertinence de ce nouveau type de communautés de liens; d'autre part, les algorithmes proposés, simples mais quadratiques avec le nombre de liens, nécessiteront une implémentation efficace
qui pourrait tirer profit d'un parallélisme en mémoire partagée (openMP, multithreading in C++0x,...).

Le stagiaire sera donc impliqué dans la compréhension des algorithmes, dans leur parallélisation et leur développement (en C++)
et dans l'analyse de données réelles à une échelle unique en Bioinformatique.

Remarques:
Ce travail se fera en contact avec le groupe Calcul (http://calcul.math.cnrs.fr/).
Il pourra faire l'objet d'une indemnité de stage.



SM110-107 Linéarité des graphes  
Encadrement  
Encadrant : Christophe CRESPELLE(écrire)
Labo/Organisme : LIP ou LIGM
Ville : Lyon ou Marne-la-Vallée

Description  
La question de trouver des représentations compactes pour les graphes, c\'est à dire prenant peu de place en mémoire, est une question centrale de l\'algorithmique de graphes, dans la théorie comme dans la pratique. Malheureusement, les méthodes de codage utilisées pour réduire la taille de la représentation en mémoire ne permettent pas toujours de traiter efficacement les requêtes faites sur les graphes, comme par exemple les requêtes de voisinage d\'un sommet, ce qui au final pénalise les algorithmes qui les manipulent.

Une façon naturelle de coder un graphe de manière compacte en conservant de bonnes propriétés algorithmiques consiste à trouver un ordre linéaire sur les sommets du graphe de sorte que pour chaque sommet, ses voisins forment un intervalle de cet ordre linéaire. Bien sûr, cela n\'est possible que pour certains graphes, appelés bi-convexes.
Afin de représenter tous les graphes de cette manière, on peut s\'autoriser plusieurs ordres linéaires et choisir un intervalle dans chaque ordre pour chaque sommet, de sorte que les voisins d\'un sommet soient exactement l\'union des intervalles choisis pour lui dans chacun des ordres linéaires. Le nombre minimum d\'ordres nécessaire pour coder un graphe de cette façon est un paramètre appelé la linéarité du graphe.

Bien que cette représentation soit naturelle, on en sait peu de choses (si ce n\'est qu\'il est NP-complet de calculer la linéarité pour les graphes quelconques). En particulier, on ne sait pas quelles sont les classes de graphes qui ont une linéarité faible, ou au contraire une linéarité élevée. Un résultat surprenant est que les classes de graphes connues pour avoir de très bonnes propriétés de codage, comme les graphes de permutation et les graphes d\'intervalles, n\'ont pas une linéarité bornée : celle-ci peut être de l\'ordre de log(n)/loglog(n). Et c\'est aussi le cas de la famille des cographes qui est pourtant une des familles les plus fortement structurées qui soit. Cela suscite un grand intérêt pour les questions suivantes : quel est exactement la linéarité de ces familles de graphes dans le pire des cas? Peut-on caractériser les graphes de linéarité bornée? ou même les graphes de linéarité 2? Peut-on calculer la linéarité en temps polynomial sur certaines classes de graphes?

Remarques:
Le stage est co-encadré par Philippe Gambette (LIGM) et Christophe Crespelle (LIP).
Il se déroulera soit à Marne-la-Vallée (au LIGM) soit à Lyon (au LIP), au choix de l\'étudiant.


SM110-109 Arithmétique générique pour OCaml  
Encadrement  
Encadrant : Michel MAUNY(écrire)
Labo/Organisme : UEI, ENSTA-Paristech
Ville : Paris

Description  
Le langage OCaml ne dispose pas d’arithmétique générique. Les opérateurs doivent en effet porter des noms différents selon qu’on les applique à des entiers ou à des flottants.

Ce stage vise à étudier la faisabilité d’une arithmétique générique pour OCaml, en regroupant les types des nombres (int, float, int32, int64) dans un type paramétré number. Le stagiaire aura à prototyper une arithmétique aussi complète que possible pour le langage OCaml et à concevoir et mettre en oeuvre les optimisations nécessaires à son efficacité. Ce travail sera concrétisé par une version expérimentale du compilateur OCaml.


Accéder au sujet détaillé

Remarques:
Ce stage est co-encadré par Benoit Vaugon et Michel Mauny.


SM110-111 Fonctions élémentaires pour circuits reconfigurables  
Encadrement  
Encadrant : Florent DE DINECHIN(écrire)
Labo/Organisme : LIP
Ville : Lyon

Description  
Elementary functions (sine, exponential, arctangent, etc) are, after the basic operations, the next useful block to be implemented to enable scientific computing on reconfigurable systems (FPGAs). Besides, it has been demonstrated (on exponential and logarithm) that their implementation in FPGAs may have a much higher performance than the software implementation in a microprocessor, at a reasonably low resource cost. The research challenge is that most of the literature addresses the imlpementation of such functions in software. The purpose of this training period is to study hardware implementations of the main functions (trigonometric, hyperbolic and their inverses) well suited to modern FPGAs. Such implementations may use small tables of precomputed values, multiplications that may be small, or rectangular, or truncated, etc. For this purpose, a good method is the creative generalization of existing algorithms.

An implementation is efficient on FPGAs if it avoids any computation that is more accurate than needed (somethings processors do all the time due to their fixed formats). This issue will be at the core of the training period.

This work will take place within the open-source FloPoCo project of ENS-Lyon:
http://flopoco.gforge.inria.fr/
FloPoCo already provides exponential, logarithm and power. It also provides meta-operators, such as a generic polynomial approximator, that will help designing the complex architectures of elementary functions. The trainee is expected to contribute to FloPoCo.

Bibliography:
J.M. Muller: Elementary functions, algorithms and implementation. Birkhauser
Hauck and DeHon. Reconfigurable computing. Morgan Kaufmann

The bibliography of the FloPoCo project is available on
http://flopoco.gforge.inria.fr/


SM110-112 Real-time Online Emulation with Simterpose  
Encadrement  
Encadrant : Martin QUINSON(écrire)
Labo/Organisme : LORIA
Ville : Nancy

Description  
Distributed systems such as grids, clusters, peer-to-peer systems, high-performance supercomputers, cloud computing infrastructures or desktop computing environments, benefit of an ever increasing popularity nowadays. Distributed applications (such as decentralized data sharing solutions, games, scientific application, high-traffic web applications or scientific computations) are executed routinely on these systems.

By nature, the resulting environments and applications are extremely complex and dynamic because they aggregate thousands of elements that are heterogeneous and shared among several users. This make these systems very challenging to study, test, and evaluate. Computer scientists traditionally study their systems a priori by reasoning theoretically on the constituents and their interactions. But the complexity of these systems make this methodology is near to impossible, explaining that most of the studies are done a posteriori through experiments.

Three main methodologies exist to experiment with computer systems: real-scale, simulation and emulation. Real-scale (or in situ) consists in executing the real application under study on an experimental platform like Grid'5000 (a large scale experimental platform in France, composed of more than 1600 machines). On the opposite, with simulation, both the application and the environments are replaced by models, and the interactions between both models are computed by a simulator. Emulation can be seen as an intermediate approach where the real application is executed within a synthetic environment. Typically, one will use a homogeneous cluster of machines as an execution environment, and use an emulation layer to reproduce the complex conditions found on the real Internet.

SimGrid (developed by the AlGorille team in collaboration) is a toolkit providing core functionalities for the simulation of distributed applications in heterogeneous distributed environments. The specific goal of the project is to facilitate research in the area of distributed and parallel application scheduling on distributed computing platforms ranging from simple network of workstations to Computational Grids. It is however not possible to use real applications directly on SimGrid: users have to extract the logic of their applications and rewrite them using the specific interfaces of SimGrid.

The Simterpose project tries to alleviate this by providing a way to use SimGrid as an emulator. This would allow real applications to be executed on virtual platforms emulated by SimGrid. This project naturally relates to the distem emulator also developed in the AlGorille team, but follows a completely different approach. Distem emulates the target platform by reducing the performance of the host platform running the experiment while Simterpose intercepts all computations and communications and delay them according to the computations of the simulator.


Accéder au sujet détaillé

Remarques:
Co-encadrement avec Lucas Nussbaum, rémunération normale prévue.


SM110-114 Preuve formelle sur l'arithmétique flottante en double arrondi  
Encadrement  
Encadrant : Sylvie BOLDO(écrire)
Labo/Organisme : INRIA Saclay - Île-de-France
Ville : Orsay

Description  
Lors de la conception d'un algorithme numérique, le choix de la précision de calcul peut jouer un rôle déterminant. Mais cette précision n'est pas forcément disponible dans tous les environnements où l'algorithme sera implanté. Par exemple, un algorithme en simple précision (float) peut se retrouver exécuté sur une architecture qui ne calcule qu'avec des nombres double précision (certains PowerPC) ou de précision plus grande encore (certains x86). Contrairement à l'intuition, l'utilisation d'une précision trop élevée peut produire des résultats d'une moins bonne qualité. Il existe cependant des méthodes, en particulier celles à base de double arrondi, qui garantissent que le résultat sera celui attendu même en cas de précision trop élevée.

L'objet du stage sera d'étudier la littérature sur ce sujet, notamment l'article de Samuel Figueroa (1995), et d'en tirer des théorèmes prouvés formellement en Coq. Le but est de trouver des conditions dans lesquelles les résultats sont inchangés et ainsi de justifier certaines transformations de code dans des compilateurs comme CompCert.


Accéder au sujet détaillé

Remarques:
Stage co-encadré par Guillaume Melquiond (guillaume.melquiond@inria.fr)

Gratification possible



SM110-117 Diffusion dans les réseaux dynamiques  
Encadrement  
Encadrant : Christophe CRESPELLE(écrire)
Labo/Organisme : LIP
Ville : Lyon

Description  
Les phénomènes de diffusion se retrouvent dans des contextes variés. Il peut s'agir de la diffusion d'une maladie dans un groupe humain, d'une information dans un groupe social ou d'un message dans un réseau informatique. La propriété qui se propage se transmet lors des contacts entre les acteurs du groupe : contacts physiques, échanges verbaux ou connexions informatiques. Dans de très nombreux contextes, les réseaux considérés sont dynamiques, c'est à dire que les contacts entre leurs protagonistes changent au cours du temps. Le but de ce stage est de comprendre les liens entre la structure de la dynamique de ces réseaux et celle des diffusions qui s'y jouent.

Ces réseaux dynamiques sont décrits par une séquence de graphes ayant tous les même sommets, représentant les acteurs du réseau étudié, mais dont les ensembles d'arêtes sont différents. On voudrait définir sur ces séquences de graphes des notions qui puissent rendre compte de la capacité d'une dynamique de graphes à favoriser ou à freiner les phénomènes de diffusion dont elle est le support. On voudrait également définir des notions capables de décrire la propension individuelle de chaque acteur de la dynamique à prendre part ou non à la diffusion qui se joue. L'équipe D-NET possède des données uniques pour apprécier la pertinence des notions envisagées : les contacts pendant 6 mois entre les centaines d'acteurs d'un hôpital à une granularité inférieure à la minute, couplés avec la donnée des souches bactériologiques qui sont portées par chaque individu de semaine en semaine.

Une notion qui paraît particulièrement prometteuse est celle de flot dans un réseau dynamique, qui évalue la quantité de substance à diffuser qui peut être transmise d'un groupe d'acteurs du réseau à un autre groupe sur une fenêtre de temps fixée. En particulier le flot entre l'ensemble des noeuds P possédant la propriété à diffuser et un noeud quelconque u du réseau peut servir à estimer à quel point le noeud u est exposé à la diffusion émanant de P. On pourra chercher à déterminer sur les données réelles si le flot est une bonne notion pour rendre compte de l'exposition d'un noeud à une diffusion : la diffusion se propage-t-elle de manière privilégiée aux noeuds fortement exposés? Y a-t-il d'autres notions que le flot plus à même de rendre compte de cette exposition? Y en a-t-il dont le calcul soit plus efficace, ce qui est crucial vu la taille des données à manipuler? Plutôt que se limiter à une fenêtre de temps pour le calcul du flot dynamique, est-il possible d'introduire un facteur d'atténuation, c'est à dire que la quantité de flot transmise dépende de la longueur du chemin parcouru depuis la source? Quelle est la bonne définition de cette notion? En quelle complexité peut-elle être calculée? Autant de questions qui pourront être examinées lors du stage.

Remarques:
Le stage est co-encadré par Eric Fleury.


SM110-118 Dynamiques des graphes de terrain  
Encadrement  
Encadrant : Christophe CRESPELLE(écrire)
Labo/Organisme : LIP
Ville : Lyon

Description  
De nombreux domaines prennent pour objet d'étude des graphes issus de contextes pratiques. C'est le cas par exemple de la sociologie, de la physique, de la biologie et bien-sûr de l'informatique. Dans ces différents contextes, souvent, les graphes étudiés ne sont pas figés, ils évoluent au cours du temps. Comprendre la structure de ces dynamiques et en concevoir des modèles pose des défis de taille et revêt des enjeux de première importance à la fois en pratique et en théorie.

Lorsque le système étudié est fermé, sa dynamique peut être représentée par une série de graphes ayant tous les mêmes sommets mais des ensembles d'arêtes différents. L'approche classique pour étudier la structure de ces séries de graphes consiste à s'intéresser à la structure de chacun des graphes qui les composent. C'est aussi l'approche suivit par la majorité des modèles de graphes dynamiques qui génèrent des séries de graphes dont les éléments ont des propriétés le plus proche possible de celles des graphes composant les séries rencontrées en pratique.

Or cette approche est insuffisante : elle ne considère pas les relations entre les différents graphes de la série et rate de ce fait une partie importante de la structure des dynamiques étudiées. Le but de ce sujet est de concevoir des modèles de dynamique qui tiennent compte des relations entre les graphes composant la série. Plusieurs approches sont possibles. Une qui paraît particulièrement prometteuse est celle qui consiste à s'intéresser à l'écart entre deux graphes consécutifs de la série (graphe dont l'ensemble d'arêtes est la différence symétrique des ensembles d'arêtes des deux graphes). Ces graphes écart contiennent une information riche sur la manière dont évoluent les graphes de la série. Actuellement, peu est connu de ces graphes et leur structure reste à caractériser. Le but de ce stage est de dégager la structure de ces graphes écart dans des cas concrets d'application et de répondre aux questions suivantes : quelle est l'influence de l'échelle temporelle à laquelle on étudie la série sur la structure des graphes écart? la structure des arêtes disparaissant en passant d'un graphe à son suivant dans la série est-elle similaire à celle des arêtes qui apparaissent? reproduire la structure des graphes écart suffit-il à reproduire la structure des graphes de la série eux-mêmes? quels sont les liens entre un graphe écart et le graphe de la série qui le précède?

Remarques:
Le stage est co-encadré par Eric Fleury.


SM110-119 Méthodes toplogiques certifiées pour l'étude des systèmes dynamiques chaotiques  
Encadrement  
Encadrant : Samuel MIMRAM(écrire)
Labo/Organisme : CEA
Ville : Paris

Description  
Les systèmes dynamiques permettent de décrire l'évolution de systèmes continus, tels que des processus physiques régis par lois décrites par des équations différentielles. Une part importante de l'étude de tels systèmes est la caractérisation des comportements limites qu'ils peuvent avoir (orbites périodiques, points stationnaires, etc), ce qui permet en particulier de déterminer si ils sont ou non chaotiques. L'objectif du stage consistera à developper un outil d'analyse des comportements limites de systèmes dynamiques en utilisant des outils mathématiques provenant de la topologie algébrique tels que l'index de Conley. Ces systèmes pouvant être chaotiques, il est crucial de prendre en compte les erreurs de calcul dûes à l'utilisation de nombres flottants, ce qui sera fait grâce l'utilisation de domaines abstraits
judicieusement choisis.


SM110-120 Homologie persistante des programmes concurrents  
Encadrement  
Encadrant : Samuel MIMRAM(écrire)
Labo/Organisme : CEA
Ville : Paris

Description  
La vérification des programmes concurrents est une tâche ardue, car il faut a priori vérifier que tous les ordonnancements possibles des sous-programmes (threads) du programme sont corrects. Cepandant, de nombreux de ces entrelacements sont équivalents dans le sens où l'on peut passer de l'un à l'autre en permutant des instructions indépendantes. Cette équivalence peut être considérée d'un point de vue géométrique en définissant une sémantique du langage dans laquelle les programmes sont interprétés par des espaces topologiques dirigés : les exécutions possibles des programmes correspondent à des chemins croissants (dans le temps) de cet espace, les trous dans ces espaces correspondent à des synchronisations entre sous-programmes (au travers de mutex par exemple) et l'équivalence entre exécutions correspond à une variante dirigée de la notion d'homotopie (déformation continue d'un chemin en un autre). L'une des difficultés dans ce cadre est d'adapter les constructions usuelles de topologie algébrique aux espaces dirigés. Récemment, la notion d'homologie (grossièrement le calcul des trous d'un espace topologique) a été étendue afin de prendre en compte des espaces dépendant d'un paramètre, ce que l'on appelle l'homologie persistante. L'objectif de ce stage consiste à utiliser cette notion afin de développer de nouveaux outils permettant de prendre en compte le temps dans les espaces topologiques dirigés et, si le temps le permet, d'expérimenter cette approche en implémentant des calculs d'homologie persistante sur les espaces interprétant des programmes concurrents.


SM110-121 Coercions monadiques  
Encadrement  
Encadrant : Samuel MIMRAM(écrire)
Labo/Organisme : CEA
Ville : Paris

Description  
Les monades permettent de structurer les langages de programmation et ont connu un grand succès depuis leur introduction en informatique par Moggi (Haskell, etc.). L'une des difficultés lors de leur utilisation dans un langage de programmation provient du fait que l'utilisateur doit explicitement utiliser des constructions pour les utiliser (et manipuler les morphisme de Kleisli associés à la monade). Il est donc naturel de se demander s'il est possible d'utiliser implicitement les monades en laissant au compilateur le soin d'insérer automatiquement des appels aux opérations de la monade. Ainsi, l'opération "return" d'une monade T pourrait être vue comme une coercion possible d'une valeur de type A en un valeur de type TA et l'opération "bind" de A->TB vers TA->TB. L'objectif du stage consistera à déterminer des conditions rendant raisonnables ces coercions associées à des monades (déterministes et universelles en particulier), en utilisant des techniques provenant de la réécriture et de la réalisabilité. Si le temps le permet, un langage fonctionnel utilisant ces coercions sera implémenté.


SM110-122 Modèles non-standard constructifs pour les systèmes hybrides  
Encadrement  
Encadrant : Samuel MIMRAM(écrire)
Labo/Organisme : CEA
Ville : Paris

Description  
Les systèmes hybrides consituent un modèle de calcul dont l'utilisation est très répandue pour modéliser, simuler et étudier des processus mélant des valeurs -- appelées flux -- dépendant de façon non nécessairement continue d'un temps continu (typiquement un réel), tels que des contrôleurs dépendant de paramètres physiques variables au cours du temps. Il est a priori difficile de définir une sémantique dénotationnelle pour ces systèmes, car certaines opérations comme l'intégration au cours du temps ne sont pas toujours définies lorsque les flux continennent des points d'accumulation de discontinuités (l'effet Zenon). Récemment, des modèles fondés sur l'analyse non standard ont été introduits, dans lesquels un système hybride est interprété par une suite d'approximations de sa sémantique, ces suites étant quotientées par une relation d'équivalence fondée sur un ultrafiltre. Cependant, la notion de convergence dans ce cadre n'est pas la notion habituelle (elle est donnée par l'ultrafiltre). L'objectif de ce stage consiste à étendre ces travaux en utilisant une version constructive de l'analyse non standard, dans laquelle l'équivalence est déterminée par un filtre, ce qui permettrait de formaliser une notion de sémantique comme suite d'approximations qui convergent au sens usuel vers une la solution attendue, dans le cas où elle est définie.


SM110-123 Aire d’une surface délimitée par les solutions d’une ou plusieurs équations polynomiales  
Encadrement  
Encadrant : Guillaume MOROZ(écrire)
Labo/Organisme : Inria Nancy - Grand Est
Ville : Villers-lès-Nancy

Description  
En robotique, de nombreux mécanismes se modélisent sous la forme de systèmes polynomiaux. Lors de leur conception, un enjeu important est de maximiser leur espace de travail. L'espace de travail d'un robot est l'ensemble des positions qu'il peut atteindre sans rencontrer d'obstacle ou de singularité. La frontière de cet espace de travail peut s'exprimer sous la forme d'un système d'équations polynomiales. Dans une approche de type essai erreur, l'enjeu est alors de calculer rapidement et précisément le volume d'un ensemble dont les frontières ne sont pas définies par des formules explicites, mais par des équations polynomiales.

Dans le cadre du stage, on se restreindra au cas où l'espace de travail est de dimension 2, et sa frontière A définie implicitement par une ou plusieurs équations polynomiales.

Le problème se ramène alors à trouver des méthodes efficaces pour calculer l'aire des composantes connexes de $[-1,1]^2\setminus A$, le
complémentaire de $A$ dans la boîte unité.

Une piste de recherche particulièrement intéressante pour ce problème est l'utilisation des polynômes de Chebyshev, qui ont notamment de bonnes propriétés d'approximation numériques.

Le candidat effectuera un travail bibliographique sur les méthodes d'intégration numériques d'une part et sur les propriétés des polynômes de Chebyshev d'autre part. Ensuite, il devra réfléchir à un ou plusieurs algorithmes de calcul d'aire adaptés aux cas A. Enfin, le candidat implantera ses méthodes (en python, maple ou c) et comparera expérimentalement leur précision et leur complexité algorithmique selon des critères objectifs.


Accéder au sujet détaillé


SM110-124 Heuristique pour régner des problèmes NP-complets sur les graphes  
Encadrement  
Encadrant : Binh-Minh BUI-XUAN(écrire)
Labo/Organisme : LIP6 - UPMC - CNRS
Ville : Paris

Description  
Un stage dans le même cadre d'étude a été proposé l'an dernier en L3, dont un apperçu est consultable au près de [Jean-Florent Raymond et al., Journées Graphes et Algorithmes, 2011]. L'objective de celui-ci est de forcer le Graal sur un deuxième point faible dans sa résistance.

Contexte général (rappel du stage 2010):
Les deux domaines de décomposition de graphes et complexité paramétrée (dite FPT - Fixed Parameter Tractability en anglais) ont connu un essor hors du commun ces dernières années, aussi bien en termes de présence dans les grandes conférences bien établies qu'en création de nouvelles conférences bénéficiant d'une communauté en expansion. Décomposer est un terme technique qui, d'un point de vue algorithmique, fait référence à la division d'une instance de calcul à des sous-instances plus "simples". Les exemples populaires de décomposition sont le Tri-Fusion et la Factorisation des polynômes. Les techniques de décomposition sont fondamentales pour les algorithmes diviser-pour-régner, ainsi que leurs variants dans la programmation dynamique. La notion de "simplicité" des sous-instances dépend de l'objectif du calcul: bien ranger une suite d'entiers pour le cas du Tri-Fusion, énumérer les racines d'un polynôme pour le cas de la Factorisation. Pour être bref, la complexité paramétrée s'adresse à des problèmes de la classe NP. Pour beaucoup de problèmes NP-complets (plus précisément ceux qui sont dans FPT: ils sont nombreux!), il s'agit d'une méthode de résolution réaliste. En théorie des graphes, la notion de "simplicité" est souvent arbitrée par une certaine mesure, appelée largeur, du (sous)graphe en question. Les largeurs de graphe bénéficient d'un appui fort des mathématiques. Dans ce sens, nous pouvons citer le théorème de Courcelle, très célèbre, qui certifie que, si nous savons comment décomposer correctement un graphe donné, tout problème exprimable en logique du second ordre sur ce graphe est dans FPT avec pour paramètre la largeur arborescente du graphe. C'est un résultat fort, parce que beaucoup de problèmes NP-complets habituels sur les graphes (Stable, Clique, Hamiltonian, Feedback Vertex Set, etc) sont bel et bien exprimables en logique du second ordre. Depuis son introduction par Robertson et Seymour, la notion de largeur arborescente a aussi connu d'énormes succès. Une requête à Google Scholar avec pour mot-clef "treewidth" convaincra certainement le lecteur. Malheureusement, la largeur arborescente est tristement célèbre pour être impuissante face aux graphes denses: typiquement, quand la donnée est un graphe complet il est pratiquement impossible d'utiliser la largeur arborescente pour résoudre p.e. Stable.

Le stage 2011:
Nous proposons dans le cadre du stage de remédier à la tristesse mentionnée. Nous étudierons l'applicabilité d'une notion récente de largeur [Bui-Xuan, unpublished]. Celle-ci connait d'excellentes propriétés de résolution pour nombre de problèmes NP-complets notoires. De plus, elle n'a pas froid aux yeux face aux graphes denses (ni aux sparses d'ailleurs). Dans ce sens, l'aboutissement de son étude fournira un vrai remède à la triste impopularité de la largeur arborescente parmi les graphes denses. Malheureusement, l'étape de décomposition liée à la nouvelle notion est difficile. Notre stage s'attaquera dans ce contexte par des heuristiques de décomposition. Il existe déjà dans la littérature de nombreux axes de recherche sur les heuristiques, et nombreux sont les notions de largeurs mises à l'étude, les principales étant arborescente, de clique, de rang, et booléenne. Il s'agit pour notre stage d'obtenir des heuristiques donnant des valeurs de largeurs plus petites que celles obtenues par tous ceux qui existent concernant les trois dernières notions dans la liste.

Objectif détaillé:
L'étude des heuristiques des décompositions a la courtoisie d'être très simple: il ne s'agit pas plus que d'arranger les sommets du graphe de départ d'une certaine façon sur les feuilles d'un arbre binaire. Ainsi, coder un heuristique est trivial, et on est vite emmené à jouer plutôt avec les formes d'arbre, un vrai jardinier!, tantôt coupant les branches, tantôt greffer celles-ci d'une façon répondant à certains critères d'esthétiques… (le jugement est arbitraire, entendu)
La nouvelle notion de largeur s'appuie sur une notion combinatoire très ancienne, dont les applications sont nombreuses, notamment en fouille de données. Concrètement, nous allons procéder en deux étapes. Dans un premier temps nous allons intégrer les techniques venant de la fouille de données. En suite, nous allons procéder à les ajuster dans le mode multi-échelles si particulier à toute étude de décomposition. Les champs d'apprentissage visés sont: théorie des graphes, algèbre booléenne, treillis de Galois.

Les connaissances et techniques plus détaillées sont disponibles à la demande.
Questions bienvenues: buixuan@lip6.fr


SM110-125 Périodicité des systèmes linéaires max-plus  
Encadrement  
Encadrant : Bernadette CHARRON-BOST(écrire)
Labo/Organisme : LIX, Ecole polytechnique
Ville : Palaiseau

Description  
Quel est le coût d’un synchroniseur dans un système distribué ? Combien de temps les trains doivent-ils attendre afin du mieux assurer les correspondances ? La théorie des systèmes max-plus est un outil pour répondre à de telles questions. Elle peut, par exemple, décrire des problèmes de transport, de processus de fabrication, de synchronisation dans les réseaux et de routage.

Une fonction linéaire max-plus F : R^n → R^n ne consiste qu’en des opérations de maximum et d’addition. Par un analogue du théorème de Perron-Frobenius dans l’algèbre max-plus, il est connu que la suite F^k(x_0) des applications répétées à un vecteur initial x_0 est finalement périodique. L’objectif de ce stage est le développement d’un logiciel pour trouver la longueur de la période et la longueur du régime transitoire d’une fonction linéaire max-plus donnée.

À chaque fonction linéaire max-plus F et à chaque vecteur initial x_0, correspond un graphe tel que les valeurs du vecteur F^k(x_0) correspondent aux chemins de longueur k et de poids maximal dans ce graphe. Certains paramètres de graphe influent sur la longueur de la période et sur la longueur du régime transitoire. Calculer ces paramètres permet d’estimer à l’avance ces longueurs, mais aussi de dessiner des stratégies optimales afin de les réduire. Le logiciel développé au cours du stage pourra être ́également utilisé pour calculer exactement le rapport entre ces longueurs et les paramètres de graphe.

Accéder au sujet détaillé


SM110-126 Absorber en couleur II  
Encadrement  
Encadrant : Laurent BEAUDOU(écrire)
Labo/Organisme : LIMOS
Ville : Clermont-Ferrand

Description  
Ce stage se situe dans la continuité du travail de Thomas Picchetti lors de son séjour dans notre équipe au printemps 2011.

Il s'agit d'approcher une conjecture attribuée à Erdös sur les tournois arc-coloriés (définitions et énoncé de la conjecture dans le document .pdf joint).

Plusieurs approches sont possibles et des sous-conjectures plus abordables sont également à traiter.

Accéder au sujet détaillé


SM110-128 1 Conception et déploiement d’une infrastructure de calcul pour le “Dilemme du Fabricant de Tables”  
Encadrement  
Encadrant : Jean-Michel MULLER(écrire)
Labo/Organisme : LIP
Ville : Lyon

Description  
En arithmétique virgule flottante (VF), avoir des opérations complètement spécifiées est une exigence-clé, si on veut développer du logiciel portable au comportement prévisible. Depuis 1985, les quatre opérations arithmétiques sont spécifiées (elles doivent être correctement arrondies: le système doit renvoyer le nombre VF le plus proche du résultat exact). Ce n’est pas tout-à-fait le cas pour les fonctions mathématiques de base: la même fonction pourra renvoyer des résultats significativement différents suivant l’environnement, avec 2 conséquences pour les logiciels utilisant ces fonctions:
• il est presque impossible d’estimer leur précision
• leur portabilité est délicate à garantir
Ce manque de spécification est dû à un problème appelé le Dilemme du fabricant de tables. Pour calculer f(x) dans un format donné, on calcule une approximation de f(x) qu’on arrondit au nombre VF le plus proche. Le problème est: quelle doit être la précision de l’approximation pour que le résultat obtenu soit toujours égal à f(x) arrondi au plus proche nombre VF? Pour résoudre ce problème, on doit déterminer, pour chaque format et fonction considérés quel est le point le plus dur à arrondir (HR- point), i.e., le nombre VF tel que f(x) est le plus proche du milieu de 2 nombres VF consécutifs. La manière naïve de résoudre ce problème (recherche exhaustive) est impraticable. Le projet TaMaDi de l’ANR, que nous coordonnons, vise à fournir:
• pour les formats et fonctions les plus courants, des tables de HR-points, avec des preuves de leur correction
• du code open-source permettant de trouver les HR-points pour d’autres formats et fonctions
l’équipe Arénaire du LIP et l’équipe CACAO du LORIA ont conçu des algorithmes (L- algorithme et algorithme SLZ) et publié des HR-points pour quelques fonctions en double précision. La complexité de leurs méthodes est exponentielle en le nombre de bits du format: elles ne peuvent être utilisées avec des formats significativement supérieurs à la double précision. Ces dernières années, Arénaire a développé une bibliothèque, CRLibm, qui implante les principales fonctions en faible précision. L’arrondi correct est fourni avec un surcoût négligeable. Ces performances ont conduit le comité de révision de la norme virgule flottante IEEE 754 à recommander (sans imposer) l’arrondi correct pour certaines fonctions mathématiques (le standard IEEE 754-2008 a été adopté en 2008). Il est donc nécessaire de calculer des HR points pour les principales fonctions mathématiques, et, si possible, pour des formats supérieurs à la double précision. Nous souhaitons le faire en mettant au point une implantation efficace de l’algorithme SLZ.
Une version expérimentale de l’algorithme SLZ a été programmée. L’algorithme (qui fait appel à l’algorithme LLL de réduction de réseaux) est basé sur divers paramètres, choisis de manière ad hoc. Trouver des paramètres qui optimisent le comportement de l’algorithme est une des grosses difficultés. L’étudiant devra:
• se familiariser avec l’algorithme SLZ, expérimenter avec le code existant pour comprendre les limites de l’algorithme et les influences des divers paramètres;
• définir des objectifs atteignables et des architectures adaptées pour les atteindre;
• repérer les faiblesses du code existant et suggérer des solutions.

Quelques liens
• l’équipeArénaireduLIP:http://www.ens-lyon.fr/LIP/Arenaire/
• le projet TaMaDi de l’ANR:http://tamadiwiki.enslyon.fr/tamadiwiki/index.php/Main_Page
• présentation vulgarisée du dilemme du fabricant de tables: http://images. math.cnrs.fr/Erreurs-en-arithmetique-des.html
• l’algorithmeSLZ:http://www.loria.fr/equipes/spaces/slz.fr. html
• une présentation de divers problèmes récents d’arithmétique des ordinateurs, et en particulier du dilemme du fabricant de tables: http://perso.ens-lyon. fr/jean-michel.muller/Conf-Journees-Knuth.pdf


Remarques:
- stage co-encadré par Nicolas Brisebarre, Guillaume Hanrot et Jean-Michel Muller

-Stage rémunéré


SM110-129 Analysis of bike sharing systems  
Encadrement  
Encadrant : Nicolas GAST(écrire)
Labo/Organisme : EPFL
Ville : Lausanne, Suisse

Description  
Bike sharing systems are giving rise to interest in the last few years. There are currently more than 400 cities around the world equipped with a bike sharing system including Lausanne, Paris, Lyon, Barcelona, Montréal, etc... One of the major issues in this system is the availability of the bikes: depending on the time of the day, some areas more popular than others and become saturated with bikes while bikes lack in other part of the city.

The goal of this project is to study temporal an spacial dependencies between stations and to build a realistic simulator. A first part of the work will be to analyze traces of traffic obtained from the city of Paris, identify bottlenecks and derive temporal or geometric patterns. Then, the goal is to build a simulator that offers a good tradeoff between complexity and accuracy and study various pricing or redistribution strategies.


Remarques:
Le stage se déroulera à l'EPFL, au sein du laboratoire LCA-2 dirigé par Jean-Yves Le Boudec. Le travail se déroulera en collaboration avec l'INRIA-Rocquencourt.


SM110-130 Structures de données compactes pour les maillages  
Encadrement  
Encadrant : Luca CASTELLI ALEARDI(écrire)
Labo/Organisme : LIX, Ecole Polytechnique
Ville : Palaiseau

Description  
Nous allons considérer le problème de représenter, de manière compacte et efficace, l'information combinatoire d'un maillage. Dans se stage on vise à concevoir de nouvelles structures de données, moins gourmandes en espace, tirant profit de certaines jolies propriétés combinatoires des graphes planaires: notamment des décompositions arborescentes connues sous le nom de forets de Schnyder.

Le but sera donc de concevoir (et éventuellement d'implémenter et tester) des représentations (statiques et dynamiques) ayant un faible cout mémoire, et permettant à la fois un accès efficace aux données (navigation en temps constant entre cellules).

Accéder au sujet détaillé

Remarques:
Co-encadrant: Gilles Schaeffer


SM110-131 Proof theory and Büchi automata  
Encadrement  
Encadrant : David BAELDE(écrire)
Labo/Organisme : ITU Copenhagen
Ville : Copenhague

Description  
Büchi automata are commonly used in verification: infinite behaviors and
specifications on such behaviors may be expressed as automata, so that the
program satisfies its specification when its automaton is included in the
specification's automaton. One may then forget about logic and focus on
designing efficient algorithms for analyzing automata. It is however desirable
that the inclusion-checking algorithm returns a certificate that can be
independently and easily checked. Better, one may hope that this certificate
corresponds to a proof in a larger framework, usable as part of complex
formalizations involving a mix of automated and interactive proof development.

We are thus interested in revisiting automata-theoretic results from the
viewpoint of logic, and more precisely proof-theory. Earlier work on finite
automata [1] illustrates that this is an interesting non-trivial program:
although formalizing existing techniques is in principle feasible, we seek
a more direct understanding which may require new notions. This kind of
approach promises to be very instructive both from the viewpoint of automata
theory and that of studying of (co)inductive proofs.

[1] David Baelde, "On the Proof Theory of Regular Formulas", TABLEAUX'09


SM110-132 Term equality in proof theory and proof search  
Encadrement  
Encadrant : David BAELDE(écrire)
Labo/Organisme : ITU Copenhagen
Ville : Copenhague

Description  
Deciding whether a logical statement holds may be done directly by enumerating
(a complete subset of) proofs, when the considered logic has good enough
proofs. This idea has driven a generalization of logic programming, leading
to the notion of uniform proof, further refined into focused proofs, which
bring a very rich proof-theoretic foundation not only for logic programming
but more generally for theorem proving.

In that perspective, it is desirable to adopt strong notions of equality that
directly reflect assumptions on terms, thanks to an elimination rule which
enumerates complete sets of unifiers. Despite successes of that approach, it
also comes with a few hard problems. In particular, unification is undecidable
in many term languages, and decidable fragments are typically not closed under
substitution, so that simple proofs may become arbitrarily complex or even
unfeasible when we instantiate them. In the end, the feasibility of a proof
may depend on the order of application of equality rules, a phenomenon that
currently escapes proof-theoretic analysis. A recent refinement of the
equality rule eliminates some of those problems, but it also complicates proof
search a lot. The purpose of this internship is to study the structure of
proofs using such a rule in various more or less simple fragments, in order to
obtain complete classes of proofs, and try to gain some insight about proof
search.


SM110-133 Les espaces de (hyper/multi)-cohérences et le développement de Taylor des lambda-termes.  
Encadrement  
Encadrant : Michele PAGANI(écrire)
Labo/Organisme : Laboratoire d'Informatique de Paris Nord
Ville : Paris

Description  
Le lambda-calcul est un modèle mathématique de la programmation fonctionnelle séquentielle. La notion de base est celle d'application d'une fonction à un argument. Une telle application est évaluée par substitution de toutes les occurrences du paramètre de la fonction par son argument [0].

L'argument peut être effacé ou copié autant de fois que nécessaire au cours de la substitution. Cette remarque simple a une interprétation mathématique attrayante au travers de ce qu'on appelle l'expansion de Taylor du lambda-calcul dans le calcul avec ressources [1,2]. Le calcul avec ressources admet une version bornée de l'application du lambda-calcul, sous la forme M(N^n), qui signifie que l'argument N est une ressource qui sera utilisée exactement n fois au cours de l'évaluation. L'expansion de Taylor traduit l'application non-bornée du lambda-calcul M(N) en la série \sum_n 1/(n!) M(N^n) d'applications avec ressources, ce qui rappelle le développement de Taylor de la fonction exponentielle.

Bien entendu, toute somme de termes avec ressources n'est pas le développement de Taylor d'un lambda-terme ordinaire, et la question de caractériser les séries qui convergent vers un lambda-terme reste à résoudre. Une réponse partielle a été apportée dans [3], dans le cadre de la logique linéaire propositionnelle, à l'aide d'un critère combinatoire caractérisant les sommes de réseaux différentiels qui convergent vers un réseau de preuve de la logique linéaire.

Ici, nous nous attaquons à cette question dans le cadre du lambda-calcul et nous cherchons une caractérisation fondée sur la sémantique dénotationnelle. Nous entendons examiner les enrichissements de la catégorie REL des ensembles et des relations décrits dans [4]. Tout ensemble S de termes avec ressources peut être interprété par une relation [[S]] dans REL. Nous nous demandons s'il existe un enrichissement C de REL tel que : [[S]] est un morphisme de C, si et seulement si, les termes de S apparaissent dans l'expansion de Taylor d'un lambda-terme.

La compréhension de la convergence à la base de l'expansion de Taylor des lambda-termes pourrait être le point de départ d'un renouveau de la notion de calcul séquentiel, représenté ici par le lambda-calcul.

[0] Krivine, Lambda-Calculus Types and Models, Masson 1993 / Girard, Proofs and Types, CUP 1989
[1] Ehrhard, Regnier, Uniformity and the Taylor expansion of ordinary lambda-terms, TCS 2006
[2] Ehrhard, Regnier, Bšhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms, CiE 2006
[3] Pagani, Tasson, The Inverse Taylor Expansion Problem in Linear Logic, LICS 2009
[4] Boudes, Non-uniform (hyper/multi)coherence spaces, MSCS 2011


Remarques:
Co-encadrant: Pierre Boudes, LIPN (http://www-lipn.univ-paris13.fr/~boudes/?lang=fr)


SM110-134 Enrichissement du programme moteur d'une animation 3D physique de quadrupède  
Encadrement  
Encadrant : Lionel REVERET(écrire)
Labo/Organisme : LJK / CNRS-INRIA - équipe MORPHEO
Ville : Montbonnot (38) - Grenoble

Description  
L'animation 3D de personnage par simulation physique consiste à contrôler le mouvement via les lois classiques de la mécanique en mettant en jeu système articulé et actuation motrice. Contrairement aux approches traditionnelles en infographie reposant sur un long travail d'édition manuelle des poses des personnages, la méthode physique permet de générer automatiquement des séquences d'animation réalistes. L'avantage de la simulation physique permet aussi de s'adapter automatiquement à toute variation d’environnement. La complexité de la modélisation rend toutefois cette méthode difficile à utiliser en production et reste encore du domaine de la recherche. Des réalisations ont été publiées dans le domaine de l'animation 3D pour les bipèdes, et récemment au sein du laboratoire en coopération avec UBC (University of British Colombia, Canada), pour les quadrupèdes. Le sujet de se stage se consacre à ce dernier cas.
Le travail effectué sur les quadrupèdes permet de générer différentes allures pour une locomotion rectiligne. La coordination motrice pour changer de direction requiert un travail supplémentaire. En se basant sur le modèle de simulation existant, le travail demandé lors de ce stage est donc de mettre au point le programme moteur permettant un contrôle stable des changements de direction du quadrupède pendant sa locomotion. On pourra partir du code existant, ou définir un nouveau simulateur en reprenant les lois de contrôles du simulateur précédent. La difficulté n'est pas d'implémenter les lois de la mécanique, mais de parvenir à un contrôle stable.


SM110-135 Programmation chimique de services Web  
Encadrement  
Encadrant : Herve GRALL(écrire)
Labo/Organisme : Ascola - INRIA, LINA - Mines de Nantes
Ville : NANTES

Description  
Pour développer des architectures à services Web ("Service-Oriented Architectures"), il faut aujourd'hui utiliser un grand nombre de langages et de technologies :
- pour l'implémentation des services~: Java, .Net, Ruby, et leurs frameworks dédiés, suivant le patrimoine applicatif,
- pour la communication~: technologies Rest, standards WS*, etc., utilisant des protocoles différents,
- pour l'orchestration des services~: BPMN, BPEL, YQL, etc., représentant des processus ou des requêtes consommant des services.
Cette hétérogénéité pose de nombreux problèmes, qui vont de la nécessité d'interfacer ces technologies pour permettre leur interopérabilité à la maîtrise des compétences.

L'objectif du stage est de réaliser une preuve de concept :
"montrer qu'il est possible de développer une architecture à services Web en utilisant UN seul langage."
Langage de programmation "chimique" répartie, il permet de définir des agents répartis, qui consomment et produisent des messages. Ces messages, qui transitent ensuite par le réseau, correspondent aux requêtes et aux réponses échangées entre les agents.

Pratiquement, le travail peut se décomposer en quatre étapes.
- Etat de l'art
- Etude du langage
- Extension du langage
- Conception et développement d'une architecture à services Web (prototype)

Accéder au sujet détaillé


SM110-136 View update translation for XML.  
Encadrement  
Encadrant : Sophie TISON(écrire)
Labo/Organisme : LIFL, INRIA Lille, équipe MOSTRARE
Ville : Villeneuve d'Ascq

Description  
Context:
In [2], we have studied the problem of update translation for views on XML documents. More precisely, given an XML view definition and a user defined view update program, the problem is to find a source update program that translates the view update without side effects on the view. Additionally, we require the translation to be defined on all possible source documents; this corresponds to Hegner's notion of uniform translation. The existence of such translation would allow to update XML views without the need of materialization.
The class of views we consider can remove parts of the document and rename nodes. Our update programs define the simultaneous application of a collection of atomic update operations among insertion/deletion of a subtree and node renaming. Such update programs are compatible with the XQuery Update Facility (XQUF) snapshot semantics. Both views and update programs are represented by recognizable tree languages. We have presented as a proof of concept a small fragment of XQUF that can be expressed by our update programs, thus allows for update propagation.
Using tree automata techniques, we have established that without constraints, ie where all source updates are allowed, all view updates are uniformly translatable and the translation is tractable.
However, the translation is a priori not functional, ie several propagations of the update on the source are in general possible.
So, we define a notion of update function - the induced relation by an update function is functional but the notion is stronger to take into account the identifiers- and we propose an algorithm to extract an update function from an update program. This algorithm is non polynomial.
Furthermore, the choice of the update on the source is somewhat arbitrary.

To Do: A first objective is the design of an "on-the-fly" version of the algorithm to improve efficiency.
A second objective is to find good heuristics to choose from a set of possible updates, a "reasonable" one.
Implementation is not required but is recommended.

Related work:

This problem can be related to the uniformization of a relation which consists in extracting from a relation a functional relation with the same domain, even if our notion of "update function" is stronger than the usual one. Our approach is a generalization of [3]. It can be also related to the following problem: given a non-deterministic transducer which can be non functional, how to evaluate it in an efficient way -here, the objective is no more to output all the possible outputs, but only one- (see e.g. [1]).


[1] Cyril Allauzen and Mehryar Mohri.
An Optimal Pre-Determinization Algorithm for Weighted Transducers.
Theoretical Computer Science, 328(1-2):3-18, November 2004.

[2] View update translation for XML, I.Boneva, B.Groz, S.Tison, A.-C. Caron, Y. Roos, et S.Staworko,
In 14th International Conference on Database Theory (ICDT), March 21-24, 2011, Uppsala, Sweden.


[3] Christian Choffrut, Serge Grigorieff, Uniformization of rational relations
(with Christian Choffrut). In "Jewels are forever", book in honor of Arto Salomaa, Springer, p.59--71, 1999.




SM110-137 Agrégation de séries temporelles de graphes  
Encadrement  
Encadrant : Christophe CRESPELLE(écrire)
Labo/Organisme : LIP
Ville : Lyon

Description  
Lorsqu'on étudie un réseau dynamique, dont les liens entre les entités changent au cours du temps, on a souvent affaire à des séries temporelles de contacts entre les noeuds du réseau : pour chaque paire de noeuds, on connaît tous les intervalles de temps [t,t'] pendant lesquels les deux noeuds considérés sont en contact. Une des approches les plus répandues pour étudier un réseau dynamique donné de cette façon par la série temporelle des contacts entre toutes les paires de noeuds consiste à agréger en un graphe les contacts ayant lieu dans une fenêtre de temps donnée. Autrement dit, on forme le graphe dont les liens sont les paires de noeuds qui sont en contact à au moins un instant de la fenêtre de temps considérée. En procédant ainsi pour un ensemble de fenêtres (généralement disjointes) de longueurs égales qui couvrent toute la durée d'étude du système, on obtient une série de graphes qui décrit la dynamique du réseau. L'intérêt de cette approche est de retrouver la structure de graphe de ces objets et de pouvoir l'exploiter.

Ainsi, quantité de travaux sur les réseaux dynamiques commencent par agréger la série temporelle des contacts décrivant le réseau en une série de graphes. Mais comment choisir la longueur de la fenêtre d'agrégation? Dans l'immense majorité des travaux scientifiques, le choix de cette période n'est pas motivé. Cela est d'autant plus surprenant que ce choix a un réel impact sur les propriétés de la série de graphes formée et sur les conclusions que l'on peut dériver par l'analyse de cette série. Dès lors, se pose la question de savoir s'il existe des périodes d'agrégation plus pertinentes que les autres et de savoir comment les trouver. C'est le but du sujet proposé.

A cette fin, on pourra se baser sur les chemins dynamiques. Un chemin dynamique dans la série des contacts est une suite de lien conduisant d'un noeud à un autre et qui sont empruntés dans l'ordre chronologique. Idem dans la série de graphes : il s'agit d'une suite de liens appartenant à des graphes dont la position dans la série va en croissant strictement le long du chemin. Pour déterminer la ou les périodes d'agrégation les plus pertinentes, il paraît naturel de s'intéresser à l'évolution de la longueur temporelle des plus courts chemins entre les paires de noeuds dans la série de graphes lorsqu'on fait varier la période d'agrégation. Un autre indicateur très prometteur est le taux d'occupation des plus courts chemins. Sur ces chemins, seuls certains pas de temps de la série de graphes sont utilisés à se déplacer, car il est plus intéressant d'attendre sur un noeud qu'il soit en contact avec un autre qui nous rapprochera de la destination du chemin plutôt que se déplacer à tout prix, y compris sur des noeuds qui nous éloigneraient du but. Le taux d'occupation est la proportion des pas de temps lors desquels on se déplace le long du chemin. Lorsque la période d'agrégation est très petite, il en va de même du taux d'occupation des plus courts chemins. Au contraire lorsque cette période devient très grande, le taux d'occupation s'approche de 1 et les chemins sont saturés. Peut-on se baser sur cette notion pour déterminer automatiquement une période naturelle d'agrégation et une période maximale au delà de laquelle on ne peut agréger sans dénaturer fortement les propriétés du réseau dynamique étudié?

Remarques:
Le stage est co-encadré par Eric Fleury.


SM110-138 Robust multiple-model fitting with J-linkage  
Encadrement  
Encadrant : Pascal MONASSE(écrire)
Labo/Organisme : LIGM-IMAGINE (Ecole des Ponts ParisTech)
Ville : Marne-la-Vallée

Description  
Context

Fitting multiple instances of a model to data that are corrupted by noise and outliers is pervasive problem in computer vision. The classical way to estimate a model from noisy data is the RANSAC algorithm. However it has been shown not to perform well for estimating multiple models and several variants have been proposed (e.g., sequential RANSAC, multiRANSAC).
An alternative is the J-Linkage algorithm, which is intrinsically designed for multiple models. It is based on a clustering method and allows finding the number of likely models in noisy data without using parameters tuning.

Objectives

We purpose to study the J-Linkage algorithm and to extend it to other model estimation task. The J-Linkage algorithm is an agglomerative clustering method that allows finding the number of models that the noisy data got without using parameters tuning.
The goal of this internship is to study and implement the J-Linkage algorithm for multiple structure estimation and to extend it to other tasks beyond multiple homography estimation. If the algorithm works fine, an online publication of the algorithm on www.ipol.im (Image Processing On-Line) could be considered.

Profile

C++ proficiency. Knowledge in computer vision and QT are a plus.

References

R. Toldo and A. Fusiello. Robust multiple structures estimation with j-linkage. Proceedings of the European Conference on Computer Vision (ECCV 2008). http://profs.sci.univr.it/~fusiello/demo/jlk/
R. Toldo and A. Fusiello. Real-time incremental J-Linkage for robust multiple structures estimation. Proceedings of the 3DPVT conference, 2010.
David F. Fouhe, Daniel Scharstein, Amy J. Briggs. Multiple Plane Detection in Image Pairs using J-Linkage (ICPR 2010).


Remarques:
Co-encadrement avec Pierre Moulon (pmoulon@gmail.com). Stage gratifié.


SM110-139 PDL Model-Checking on Trees  
Encadrement  
Encadrant : Sylvain SCHMITZ(écrire)
Labo/Organisme : LSV, ENS Cachan
Ville : Cachan

Description  
Propositional Dynamic Logic (PDL) on trees, aka Regular XPath, is a widely used formalism to reason on trees. It has numerous applications in linguistics, databases, and verification. Although the PDL model-checking of a single tree can be carried out efficiently in PTime, the model-checking of a regular set of trees and the satisfiability problems suffer from a general ExpTime-hardness complexity.

Objective: Decision procedures for PDL on trees often rely on the construction of tree automata. Here the issue is that a naive implementation of these algorithms is too explosive, and a symbolic representation of the state space of the automaton is required. Some typical techniques could be employed to this end: binary decision diagrams, which have been very successful in verification problems, and antichain representations, which are less well investigated on tree automata. Using a symbolic representation is only the beginning of the story: we next need algorithms working directly on this representation for the most important operations: emptiness, intersection, Hadamard product, etc. These ideas have to be implemented in order to demonstrate their practical value.


Accéder au sujet détaillé


SM110-140 Formalisation de la marche dans les triangulations  
Encadrement  
Encadrant : Yves BERTOT(écrire)
Labo/Organisme : INRIA Sophia Antipolis
Ville : Sophia Antipolis

Description  
Dans une triangulation, il existe un critère pour se déplacer d'un triangle à un voisin en direction d'un point cible. Ce critère ne garantit l'aboutissement de la marche que si la triangulation possède la propriété de Delaunay. Le but de ce stage sera de décrire une preuve de cette notion en utilisant le système Coq. La preuve ne demande que des connaissances simples de géométrie (puissance d'un point par rapport à un cercle) mais il est important de comprendre comment ces connaissances peuvent être combinées avec la structure de données utilisée pour représenter la triangulation.



SM110-141 Call-by-value and call-by-name calculi: syntax, semantics, and logics  
Encadrement  
Encadrant : Stefano GUERRINI(écrire)
Labo/Organisme : LIPN, Istitut Galilée, Paris 13
Ville : Villetaneuse

Description  
Call-by-name and call-by-value are the two main mechanisms for passing arguments to functions in programming languages. The λ-calculus is the core syntax for studying properties of the evaluation paths (reductions) of call- by-name and call-by-value, while linear logic gives the tools for a careful logical interpretation of call-by-name and call-by-value. The aim of the internship is to survey the vast literature on the topic and to envisage developments from one of these three possible points of view: Logic. In the last years, several calculi have been proposed basing on the fact that call-by-value can be seen a sort of De Morgan dual of call-by-name. A possible direction for the internship might be to analyse in detail and to compare how this logical duality is exploited in the different cases. Syntax. Call-by-value and call-by-name correspond to two distinct translations of intuitionistic implication into linear logic, and therefore to two different encodings of λ-calculus into linear logic proof nets. A possible direction for the internship might be to study call-by-value and call-by-name directly on proof nets, especially by taking into account the new correspondences recently discovered between proof nets and calculi with explicit substitutions. Semantics. Denotationalmodelsofcall-by-nameandcall-by-valuecanbeconstructedbysolvingdomainequations: the difference between call-by-name and call-by-value being the equation to be solved. Pitts has given a general technique for proving adequacy of equation solutions which works for both call-by-name and call-by-name. A possible direction for the internship might be to investigate if and how this technique may be extended to proving full abstraction. The internship is directed to M2 and M1 students. In particular, for M2 students, the internship might be the starting point for a PhD thesis on a related subject (this might subject to the availability of grants from the PhD school of the Institut Galil ́ee of Paris 13). During their internship the student will be hosted by the equipe LCR (Logic, Computation and Logic) of the CNRS UMR LIPN (Laboratoire d’Informatique de Paris Nord) of the Institut Galil ́ee of Paris 13 University. LIPN may allocate a grant to students which are not funded from other institutions. The complete proposal is available at http://www.lipn.univ-paris13.fr/~guerrini/stages/cbv-cbn.pdf or on the internship section of the LCR team web page http://www.lipn.univ-paris13.fr/LCR.

Accéder au sujet détaillé

Remarques:
Co-encadrant: Giulio Manzonetto giulio.manzonetto@univ-paris13.fr Possibilité de rémunération. Possibilité de poursuite en thèse (peut être soumis à l'allocation d'une bourse de thèse par l'école doctorale de l'Institut Galilée)


SM110-142 Preuve formelle pour clusteurs de gènes  
Encadrement  
Encadrant : Binh Minh - Frederic BUI XUAN - PESCHANSKI(écrire)
Labo/Organisme : Lip6
Ville : Paris

Description  
De nos jours, l'interaction intrinsèque entre deux domaines importants de la recherche scientifique, la génétique et l'algorithmique, n'a plus besoin d'un long discours. Celle-ci tient une place importante non seulement dans la production scientifique, les réalisations en laboratoire, mais aussi dans la vulgarisation à la connaissance populaire. Le but de ce stage est d'utiliser un assistant de preuve (Coq, Isabelle, HOL Light, etc.) dans l'objectif de fournir une preuve formelle, constructive et vérifiable automatiquement de la correction d'un algorithme fondateur en bio-informatique: l'algorithme de Uno et Yagiura.

Un gène, à la louche, est un morceau dans une structure plus ou moins linéaire représentant le génome d'une certaine espèce. Un groupement de gènes de l'espèce alpha est un ensemble de gènes dont les occurrences se présentent côte à côte quelque part dans son génome. Baladeur et joueur, un gène peut avoir des occurrences dans les génomes d'autres espèces; ainsi, on peut parler de groupement de gènes commun à plusieurs espèces, alpha, beta, gamma, etc. On s'adresse à ces groupements sous le nom de clusteurs de gènes (de alpha, beta, gamma, etc). Cette notion est fondamentale et a conduit à non seulement des généralisations, spécialisations et de nombreux variantes, mais aussi à des applications inattendues dans l'histoire de l'évolution et la sélection des espèces. Ne serait-ce que dans le domaine algorithmique, des dizaines d'articles scientifiques dans de grandes revues ont vu le jour autour de ce sujet dans la dernière décennie. Pourtant, son histoire ne remonte pas si loin...

Dans les années 90, Uno et Yagiura ont proposé le premier formalisme pour calculer les clusters de gènes sous certains conditions simples et réalisables en laboratoire. Ils ont proposé également plusieurs programmes pour ce calcul, dont un est rendu célèbre par la suite dans les communautés, aussi bien bioinformaticiens qu'algorithmiciens. Le programme en question a un temps d'exécution hors norme, et semble toujours donner des réponses justes. Pourtant, son analyse théorique est très difficile, ainsi, Uno et Yagiura ont soumis leur papier à Algorithmica, pour une acceptation et publication.. presque cinq ans plus tard [Uno et Yagiura, Algorithmica, 2000]. Malheureusement, la version de la preuve de complexité et, plus important dans la pratique, celle de correction de l'article original n'a pas été convaincante, sa brièveté (en ~10 lignes) n'avait certainement pas aidé. Des années passent et nombreux ont été des études mettant l'algorithme Uno-Yagiura en pratique (il tourne quand même très vite, même sur des données de taille astronomique), mais aucun n'a fournit de preuves plus convaincantes. Si bien qu'en 2005, une équipe de recherche franco-québécoise a proposé un algorithme alternatif, ayant le même ordre de grandeur de performance [Bergeron et al., 2005]. Une autre étude parallèle à la même année, en revanche, proposait de revisiter les preuves de Uno-Yagiura, et aboutissait à des preuves théoriques convaincantes, basées sur invariants et propriétés structurelles [Bui-Xuan et al., 2005]. Ce sont ces propriétés que nous souhaitons formaliser dans un assistant de preuve, pour ainsi rendre quasiment irréfutable la preuve de correction, et ainsi redonner ses lettres de noblesses théoriques à cet algorithme incroyablement pratique. En effet, l'algorithme Uno-Yagiura est toujours de loin l'algorithme le plus utilisé en pratique et le fondateur de nombreux d'autres. Ses applications ne restent pas seulement dans le domaine bioinformatique, mais aussi en combinatoire énumérative et en génération aléatoire, en passant par la théorie des graphes.

Objectifs détaillés:
L'algorithme Uno-Yagiura possède une version naïve. Un encodage (sous Isabelle) de celle-ci est déjà bien avancée, et son assimilation nous servira comme une excellente introduction aux paysages. Ensuite, nous effectuerons une "remontée" à l'algorithme optimisé en deux temps, car il existe une version intermédiaire idéalement située entre les deux extrêmes. Finalement la preuve de correction tant attendue sera construite. En guise de bonus et si le temps le permet, il sera possible de se lancer dans l'extraction automatique d'une implémentation certifiée de l'algorithme, en commençant par la version naïve.

Apports du stage:
Outre l'apprentissage et le travail en preuve formelle en soi, cette initiative apportera des connaissances en algorithme de texte (voire de graphe), combinatoire sur les permutations, fonction génératrice des intervalles, etc. Les connaissances et techniques seront amplement fournis par les encadrants: en algorithmique/combinatoire (Bui-Xuan) en algorithmique/preuve formelle (Peschanski).

Questions bienvenues: buixuan@lip6.fr frederic.peschanski@lip6.fr

Quelques liens:
- Coq proof assistant : http://coq.inria.fr/
- Isabelle proof assistant : http://www.cl.cam.ac.uk/research/hvg/isabelle/
- HOL light : http://www.cl.cam.ac.uk/~jrh13/hol-light/
- Certified Programming with Dependent Types : http://adam.chlipala.net/cpdt/


SM110-143 Surfaces de Subdivision Généralisées  
Encadrement  
Encadrant : Bernard MOURRAIN(écrire)
Labo/Organisme : GALAAD, INRIA
Ville : Sophia Antipolis

Description  
Les surfaces de subdivision sont basées sur des constructions géométriques très simples. A partir d’un ensemble initial de points (dit de contrôle) et de facettes les reliant, de nouveaux points sont calculés par combinaison linéaire de points voisins puis insérés dans certaines faces. Cette construction est appliquée récursivement et la surface limite est appelée surface de subdivision. En pratique, cette construction appliquée jusqu’à un certain niveau fournit une bonne approximation d’une surface de subdivision et elle est très rapide à calculer.

De part leur capacité à décrire des formes géométriques complexes et leur faciliter à les contrôler, les surfaces de subdivision sont maintenant très utilisées en graphique et en particulier en animation.

L’objectif de ce stage est d’étudier et d’expérimenter une généralisation de ces constructions dans le cas où des informations supplémentaires de tangence sont prises en compte dans la subdivision. Ces schémas devraient conduire à des surfaces dont la régularité est mieux contrôlée que dans les surfaces de subdivision classiques. Il s’agit ainsi d’obtenir des constructions plus adaptées aux problèmes de modélisation géométrique tels qu’ils apparaissent en conception assistée par ordinateur ou en calcul scientifique.

Le travail se divisera en une partie d’analyse de quelques travaux existants, d’une partie d’implémentation et d’expérimentation graphique à l’aide du modeleur géométrique Axel et enfin d’une synthèse des pistes explorées et résultats obtenus.



Remarques:
Possibilité de rémunération.


SM110-144 Logique de transformations de graphes  
Encadrement  
Encadrant : Ralph MATTHES(écrire)
Labo/Organisme : IRIT (UMR5505)
Ville : Toulouse

Description  
Le stage a pour but de développer des méthodes de raisonner sur des
transformations de graphe. Des transformations de graphes
interviennent dans plusieurs domaines: dans des programmes manipulant
des pointeurs; dans l'ingéniérie dirigée par des modèles (où les
modèles sont représentés par des graphes et les transformations sont
des actions tels que le refactoring, la linéarisation etc); dans des
réseaux de communication, où des altérations du réseau (défaillance de
routers) peuvent être perçues comme transformations.

Dans tous les cas, on s'intéresse à prouver que certaines propriétés
sont préservées ou établies par les transformations, par exemple la
connectivité du graphe, l'atteignabilité d'un noeud par un autre, ou
certaines propriétés topologiques (planarité, exclusion de mineurs
etc.).

Dans l'immédiat, le stage se concentrera sur l'utilisation d'approches
de méthodes automatiques étudiées dans la littérature et de méthodes
développées dans l'équipe d'accueil. Selon les intérêts du / de la
stagiaire, le stage pourra se poursuivre à raffiner ces méthodes (donc
de se confiner au plan théorique), de proposer des implantations
efficaces des méthodes d'inférence ou d'intégrer les méthodes dans des
assistants de preuve interactifs (notamment Coq ou Isabelle).

Accéder au sujet détaillé

Remarques:
Co-encadrement par Ralph Matthes (CNRS) et Martin Strecker (Université Paul Sabatier).

Ce stage fait partie d'une thématique plus large de raisonnement sur
des graphes, abordée dans le projet ANR Climt. Ce projet démarrera en
février 2012. Le stage sera rémunéré / gratifié.


SM110-145 Problèmes de partition: résolution par la méthode des plans-coupants  
Encadrement  
Encadrant : Vincent LIMOUZY(écrire)
Labo/Organisme : LIMOS
Ville : Clermont-Ferrand

Description  
L'objectif de ce stage est d'étudier des problèmes de partitions de structures combinatoires (i.e. graphes, ensemble) étant donné un fonction objectif, trouver une partition de l'objet considéré de coût le plus faible.

Ce problème a des applications pour le problème du re-découpage des circonscriptions électorale.

Les détails sont disponibles à l'adresse suivante:
http://www.isima.fr/~limouzy/StagesM1/partition.pdf

Accéder au sujet détaillé

Remarques:
Le stage est co-encadré par Mourad BAIOU et Vincent LIMOUZY.


SM110-146 Langages de pavages temporisés 1D  
Encadrement  
Encadrant : David JANIN(écrire)
Labo/Organisme : LaBRI, Université de Bordeaux
Ville : Talence

Description  
La recherche d’expressions rationnelles pour les langages temporisés [1] a fait l’objet de nombreux travaux [2,3].

Nous proposons ici d’étudier les langages temporisés via la notion de langages rationnels de pavages temporisés : sortes d’extensions au cas temporisé des langages rationnels de pavages de dimension un.

Pour ce faire, on pourra s’appuyer sur les travaux déjà réalisés, dans le cadre non temporisé, autour des parties rationnelles du monoïde de McAlister [5] et des automates boustrophédons (two-way automata) [6,4] en y ajoutant des filtres temporels à la manière d’Asarin et al. [2,3].
L’extension temporisé du monoïde quasi-inversif des pavages unidimensionnels, sous monoïde du monoïde de McAlister, plus adapté à la définition d’une notion pertinente de langages reconnaissables, pourra aussi être considérée.
Déjà fort intéressante d’un point de vue strictement théorique, cette étude pourrait aussi, en pratique, conduire au développement de contrôleurs temps-réel avec anticipations, fort utile pour la modélisation de flux musicaux interactifs contrôlés temps-réel.

1. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2) :183–235, 1994.

2. Eugene Asarin, Paul Caspi, and Oded Maler. Timed regular expressions. J. ACM, 49(2) :172–206, 2002.

3. Eugene Asarin and Catalin Dima. Balanced timed regular expressions. Electr. Notes Theor. Comput. Sci., 68(5) :16–33, 2002.

4. Jean-Camille Birget. Concatenation of inputs in a two-way automation. Theoretical Computer Science, 63(2) :141 – 156, 1989.

5. Mark V. Lawson. McAlister semigroups. Journal of Algebra, 202(1) :276 – 294, 1998.

6. Jean-Pierre Pécuchet. Automates boustrophedon, semi-groupe de birget et monoide inversif libre. ITA, 19(1) :71–100, 1985.


SM110-147 Intégration de Z3 en Coq  
Encadrement  
Encadrant : Chantal KELLER(écrire)
Labo/Organisme : Laboratoire Informatique Polytechnique
Ville : Palaiseau (France)

Description  
Les prouveurs SMT sont des outils automatiques de démonstration très puissants, mais peu fiables. A contrario, les assistants de preuve tels que Coq sont très sûrs, mais peu automatisés. SMTCoq est un outil permettant de bénéficier de l'automatisme des prouveurs SMT dans Coq sans en compromettre la sûreté. Le but du stage est d'intégrer le prouveur SMT Z3 (développé à Microsoft Research) dans SMTCoq.

Accéder au sujet détaillé

Remarques:
Co-encadrant : Benjamin Werner (LIX)


SM110-148 machine learning under constrained budget for green computing  
Encadrement  
Encadrant : Ludovic DENOYER(écrire)
Labo/Organisme : LIP6 - Université Paris 6
Ville : Paris

Description  
Automated tools for machine learning are usually designed to maximize performance criteria like
classification accuracy or ranking maximization, regression error minimization, etc .... The learning criterion of quality is directly integrated into a training loss to be optimized via some optimization technique like optimization algorithms or gradient descent for example. However, for many modern applications, real learning criteria should also consider external constraints such as computation time, memory usage, features or data acquisition, or even very concrete external factors such as power consumption, development time, cost of maintenance etc .... These different criteria are difficult to model and cannot be taken into account by considering only the classical machine learning approach. This is a new problem in machine learning, which is emerging in the context of the Big Data framework, where huge quantities of data have to be processed for different types of applications.


The internship will focus on the development of simulation‐based methods allowing the simultaneous consideration of various complex criteria. The case study considered will be that of search engines and indexing problems: typically, the methods used by companies like Google now consist in very large indexes for rapidly calculating the relevance scores. This requires large computer farms that consume very large quantities of energy doing which represent nowadays critical resources. We will explore new
methods for budget learning, i.e. learning under external constraints for discovering automatically search methods able to reach providing a certain search quality, within a limited energy budget.


Remarques:
Co-Encadrement: Patrick Gallinari
Rémunération Possible



SM110-149 Familles de graphes et modèles de chevauchements  
Encadrement  
Encadrant : Vincent LIMOUZY(écrire)
Labo/Organisme : LIMOS
Ville : Clermont-Ferrand

Description  
Le but de ce stage sera d'étudier les classes de graphes qui admettent un modèle de chevauchement.

Dans un premier temps, l'attention sera porté sur les graphes de chevauchement d'arcs autour d'un cercle. Il s'agira de déterminer étant donné
un graphe non orienté, si on peut réaliser ce graphe avec le modèle de chevauchement. On se posera la question de la reconnaissance. Est ce qu'il existe un algorithme polynomial ou est ce que ce problème est NP Complet.

Plus de détails sont disponibles dans le document
situé là: http://www.isima.fr/~limouzy/StagesM1/overlap.pdf

Accéder au sujet détaillé


SM110-150 Rétro-ingénierie de modèles comportementaux par apprentissage automatique  
Encadrement  
Encadrant : Nicolas BASKIOTIS(écrire)
Labo/Organisme : LIP6 - UPMC
Ville : Paris

Description  
Les modèles de spécification de scénarios comme les diagrammes de séquence représentent un moyen très utile pour la compréhension d'un système et de son comportement. Quand ces diagrammes sont absents ou obsolètes, la rétro-ingénierie est utilisée pour extraire
semi-automatiquement ce genre de modèles.
Ce stage propose d'explorer des méthodes de rétro-ingénierie automatiques par apprentissage statistique.

Les algorithmes actuels s'inspirent fortement des techniques d'inférence grammaticale. Le coeur du processus consiste à inférer un automate représentant le diagramme de séquence à partir de traces. Ces méthodes nécessitent soit l'intervention d'un expert pour guider l'inférence de l'automate, soit la mise en place d'heuristiques pour le controle de la généralisation, souvent trop spécifiques produisant des diagrammes très complexes et non utilisables.

L'idée principale que nous souhaitons développer dans ce stage consiste à utiliser des méthodes de l'apprentissage statistique afin de considérer des fusions ``bruitées'' d'états.
Deux pistes prometteuses pourront être explorées lors du stage. La première, inspirée de l'inférence de modèles de markov caché, consiste à apprendre les probabilités de transitions séquence par séquence, puis d'élaguer les transitions peu prometteuses. La seconde, inspirée de la recherche de motifs fréquents, consiste à fusionner/clusteriser les états par blocs de manière hiérarchique en fonction d'un critère de granularité reflétant le degré de ``bruit'' ou d'approximation autorisé.


Accéder au sujet détaillé

Remarques:
Co-encadrement : Sylvain Lamprier (LIP6/UPMC)

possibilité de rénumération.


SM110-151 Preuves automatiques d'équivalence de programmes en Coq  
Encadrement  
Encadrant : Nicolas TABAREAU(écrire)
Labo/Organisme : École des Mines de Nantes
Ville : Nantes

Description  
Ce stage porte sur le problème de l'équivalence de programmes dans un fragment de ML comprenant références d'ordre supérieurs et exceptions. Pour cela, nous utiliserons les récents développements sur les relations logiques utilisant des mondes basés sur des STSs (State Transition Systems) [1] et la construction modulaire de telles relations à l'aide du forcing [2] pour définir des règles d'inférence permettant de prouver de telles équivalences.

Il s'agira alors de définir une procédure de décision se basant sur ces règles d'inférences, qui collectera les contraintes puis les résoudra à l'aide d'un solveur SMT.
Ce problème étant de manière générale indécidable, la procédure sera uniquement correcte mais non complète.

Finalement, on considérera l'écriture d'une tactique Coq issu de cet procédure de décision.

[1] D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. ICFP'10
[2] G. Jaber, N. Tabareau. Decomposing Logical Relations with Forcing http://hal.inria.fr/hal-00585717

Remarques:
Possibilité d'hébergement gratuit à la Maison des Élèves.


SM110-152 Hadoop MapReduce et Systèmes de Fichiers Distribués  
Encadrement  
Encadrant : Fabrice HUET(écrire)
Labo/Organisme : INRIA
Ville : Sophia-Antipolis

Description  

Map-Reduce est un modèle de programmation inspiré des primitives map et reduce qu'on trouve dans les langages fonctionnels. Proposé par Google[1] il permet de traiter de larges quantités de données sur une infrastructure distribuée de type cluster en distribuant l'exécution des map et des reduce.

Hadoop[2] est une implémentation Open Source en Java de MapReduce sponsorisée par la fondation Apache. Il est composé de plusieurs modules qui ont chacun un rôle important dans l'infrastructure. Le premier, HDFS, implémente un système de fichier distribué. Les données sont découpées en blocs qui sont ensuite répartis sur différentes machines, avec de la redondance. Le deuxième, MapReduce, implémente la gestion et l'exécution des taches Map et Reduce définies par l'utilisateur. HDFS est un système de fichier extrèmement basique. Il a un unique point de pannes (le NameNode) et ne supporte pas la modification de fichiers en place. L'ajout de données en fin de fichier est supporté à titre expérimental. Une autre limitation importante d´Hadoop est que les noeuds de stockage et les noeuds de calculs doivent être les même. L'idée est qu'un noeud de calcul va autant que possible essayer de traiter les données locales pour des raisons de performance. En pratique cependant, le scheduling est extrèmement basique et très peu de taches utilisent les données locales.

Le but de ce stage est, dans un premier temps, de modifier Hadoop pour lui permettre d'utiliser d'autres systèmes de fichiers distribués [3,4,5] à la place d'HDFS. C'est un travail technique qui nécessite une bonne connaissance en Java et en C (Prog Système).

Dans un deuxième temps, il sera intéressant de voir comment améliorer le scheduling pour augmenter la proportion de taches traitant des données locales.


References :
[1] Jeffrey Dean and Sanjay Ghemawat. 2008. MapReduce: simplified data processing on large clusters. Commun. ACM 51, 1 (January 2008)

[2] Hadoop, http://hadoop.apache.org/

[3] GlusterFS, http://www.gluster.org/

[4] Ceph, http://ceph.newdream.net/

[5] Lustre, http://wiki.lustre.org/index.php/Main_Page



Remarques:
Rémunération et aide au logement


SM110-127 Affectation de fréquences et coloration de graphes  
Encadrement  
Encadrant : Frédéric MAFFRAY(écrire)
Labo/Organisme : G-SCOP (Grenoble INP)
Ville : Grenoble

Description Sujet choisi par tienne PY-CIRCAN  

Dans un réseau de télécommunications qui consiste en des émetteurs placés en divers lieux, on doit affecter une fréquence à chaque émetteur de manière à respecter des contraintes de non-interférence : les fréquences sont représentées par les entiers ; deux émetteurs "proches" l'un de l'autre doivent avoir des fréquences différentes, et deux émetteurs "très proches" doivent avoir des fréquences dont la différence est au moins 2.
On désire minimiser le nombre lambda de fréquences à utiliser.
Cette situation peut être modélisée par une variante du problème de la coloration des sommets d'un graphe. Il est connu que ce problème (déterminer la valeur exacte de lambda pour chaque graphe) est NP-complet en général. Des bornes qui encadrent la valeur de lambda ont été données dans certains cas.

L'étudiant devra se familiariser avec le problème en étudiant les résultats connus. Il pourra ensuite attaquer des questions ouvertes concernant ce problème.


Alexandre Miquel

Valid HTML 4.01 Transitional