|
SM207-1 Analyse statique de programme par interprétation abstraite
|
|
|
Description
|
|
L'analyse de programmes par interprétation abstraite calcule de façon sûre des propriétés vraies pour toutes les exécutions de programmes, à l'aide de représentations symboliques (polyèdres convexes, formules de logique, automates finis..) de sur-ensembles des états possibles du programme. La difficulté consiste à garder une bonne précision (obtenir des petits invariants, permettant de démontrer les propriétés désirées) tout en gardant une bonne complexité (temps et espace), sachant que les problèmes considérés sont souvent indécidables ou NP-durs.
L'outil actuel développé dans l'équipe (PAGAI( fait un certain nombre d'approximations pendant l'analyse. Ces approximations sont en général conservatives, donc produisent des invariants justes, mais sous-optimaux. Parmis les améliorations possibles, nous pensons à :
Une analyse plus raffinée des programmes avec pointeurs ou tableaux
Une meilleure gestion des relations entre les variables booléennes et numériques
De meilleures heuristiques de parcours du graphe de flot de controle du programme
Une meilleure utilisation du SMT-solveur, en simplifiant la formule à résoudre avant de lancer le solveur
Une meilleure gestion des nombres flottants
...
L'étudiant commencera par se familiariser avec l'interprétation abstraite en général, et l'outil Verimag en particulier, puis choisira un ou plusieurs des points ci-dessus. Ces fonctionalités seront conçues, implémentées, puis testées sur les benchmarks existants.
URL sujet détaillé : http://www-verimag.imag.fr/M2R-Info-2012-2013-Analyse.html
Remarques : Stage indemnisé selon dispositions réglementaires. Possibilité de poursuite en thèse financée.
|
|
|
|
|
|
SM207-2 Analyse modulaire de programmes
|
|
|
Description
|
|
L'analyse automatique de programmes permet de démontrer l'absence de certains problèmes (p.ex. débordements de tableaux, dépassements arithmétiques) avant de lancer effectivement les programmes, ce qui est précieux pour certaines applications (p.ex. aéronautique). Elle diffère du test en ce que le test ne vérifie qu'un nombre fini de cas et peut donc laisser passer des problèmes.
Une des difficultés pour analyser des programmes de grande taille est la croissance du coût (temps, mémoire) des algorithmes d'analyse avec la taille du code et le nombre de variables. Pour conserver des coûts tolérables, il est nécessaire de procéder modulairement : réaliser des analyses sur des parties du programmes assez indépendamment les unes des autres.
Certaines techniques modulaires se basent sur des limites syntaxiques du programme source : on va analyser fonction par fonction, classe par classe, etc. Ces critères sont peu pertinents dans le cas de certains types de logiciels, notamment ceux de contrôle synchrone tels qu'utilisés en avionique, où ce seraient plutôt des réseaux de dépendances entre variables qui devraient être étudiés. L'objet du stage est de concevoir, étudier et implanter des heuristiques de découpage modulaire.
URL sujet détaillé : http://www-verimag.imag.fr/M2R-2012-2013-Analyse-modulaire-de.html
Remarques : Stage indemnisé selon dispositions réglementaires. Possibilité de poursuite en thèse financée.
|
|
|
|
|
|
SM207-3 Analyse de programme efficace
|
|
|
Description
|
|
L'analyse automatique de programmes permet de démontrer l'absence de certains problèmes (p.ex. débordements de tableaux, dépassements arithmétiques) avant de lancer effectivement les programmes, ce qui est précieux pour certaines applications (p.ex. aéronautique). Elle diffère du test en ce que le test ne vérifie qu'un nombre fini de cas et peut donc laisser passer des problèmes.
Une des difficultés pour analyser des programmes de grande taille est le très grand nombre de chemins possibles dans le code : soit on " mélange " des résultats d'analyse de chemins différents (ce qui peut donner des résultats décevants et empêcher de démontrer des propriétés pourtant vraies), soit on les traite séparément, ce qui peut être très coûteux. Heureusement, dans la dernière décennie, des algorithmes de décision rapides ont été développés. L'objectif de ce stage est de les exploiter au mieux.
Il s'agit d'introduire des procédures de décision dans la résolution de certains problèmes (calcul d'invariants par itération de politique, calcul de variants pour prouver la terminaison...) pour lesquels les algorithmes précédemment connus procèdent par énumération explicite des chemins.
URL sujet détaillé : http://www-verimag.imag.fr/M2R-2012-2013-Analyse-de-programme.html
Remarques : Stage indemnisé selon prescriptions réglementaires. Possibilité de poursuite en thèse financée.
|
|
|
|
|
|
SM207-4 Optimisation de formules SMT
|
|
|
Description
|
|
On sait décider (assez efficacement) la satisfiabilité de formules logiques portant sur l'arithmétique entière (linéaire), réelle, ou encore sur des entiers binaires de taille fixée. Ceci est très utile pour l'analyse automatique de programmes (recherche automatique de bugs, abstraction par prédicats...), où l'on exprime les traces d'exécution de programme ayant certaines propriétés (p.ex. mener à un bug) comme des solutions de telles formules.
Malheureusement, certaines classes de formules, par ailleurs très faciles à construire et qui arrivent naturellement dans certains problèmes d'analyse de programmes, font exploser la complexité des procédures de décision usuelles. Cependant, il est souvent possible de réarranger ces formules par ajout de contraintes " superflues " mais qui accélèrent grandement le calcul.
L'objet du stage est d'étudier un mécanisme automatique pour faire cela, au moins pour certains types courants de formules.
URL sujet détaillé : http://www-verimag.imag.fr/M2R-2012-2013-Optimisation-de.html
Remarques : Stage indemnisé selon prescriptions réglementaires. Possibilité de poursuite en thèse financée.
|
|
|
|
|
|
SM207-5 Décision de formules contenant des flottants
|
|
|
Description
|
|
On sait décider (assez efficacement) la satisfiabilité de formules logiques portant sur l'arithmétique entière (linéaire), réelle, ou encore sur des entiers binaires de taille fixée. Ceci est très utile pour l'analyse automatique de programmes (recherche automatique de bugs, abstraction par prédicats...), où l'on exprime les traces d'exécution de programme ayant certaines propriétés (p.ex. mener à un bug) comme des solutions de telles formules.
Malheureusement, certaines classes de formules, par ailleurs très faciles à construire et qui arrivent naturellement dans certains problèmes d'analyse de programmes, font exploser la complexité des procédures de décision usuelles. Cependant, il est souvent possible de réarranger ces formules par ajout de contraintes " superflues " mais qui accélèrent grandement le calcul.
L'objet du stage est d'étudier un mécanisme automatique pour faire cela, au moins pour certains types courants de formules.
URL sujet détaillé : http://www-verimag.imag.fr/M2R-2012-2013-Decision-de-formules.html
Remarques : Stage indemnisé selon prescriptions réglementaires. Possibilité de poursuite en thèse financée.
|
|
|
|
|
|
SM207-6 Physical attacks and code-based cryptosystems
|
|
|
Description
|
|
Most of the cryptographic schemes used and studied today are based on number theory problems as factorisation or discrete logarithm. In 1994, Shor proposed an algorithm which can factorise in polynomial time using a quantum computer. So RSA and several others schemes are threatened by the quantum computer.
Code-based cryptography is one of the branches of post-quantum cryptography with lattice-based, multivariate-based and hash-based cryptography. Schemes based on problems as syndrome decoding or decoding random codes are well studied for years and there doesn't exist polynomial time algorithm to solve those problems even in a post quantum world. McEliece was the first to propose a code-based cryptosystem and several improvements and derivation have been proposed so far.
To consider the use of code-based cryptosystems in the real life, they must be resistant to physical attacks as power analysis or fault injection. To date, the study of such attacks on such schemes are rare and there is a lot of work to do in this area.
After a state of the art of code-based schemes and side-channel attacks the student will implement an attack even on smart card, FPGA, graphic card or CPU.
Both practical and theoretical, this thesis proposes to study the physical attacks also called side-channel attacks like Simple Power Analysis, Differential Power Analysis, Higher-Order-Differential Power Analysis or Fault Attack and to show how we can apply these patterns to attack code-based cryptosystems like Courtois-Finiasz-Sendrier signature scheme, Stern's zero-knowledge identification scheme or McEliece public key cryptosystem.
URL sujet détaillé : http://www.cayrel.net/enseignement/2012-2013/article/physical-attacks-and-code-based-261
Remarques :
|
|
|
|
|
|
SM207-7 Multiscale tissue simulation
|
|
|
Description
|
|
ODE modeling is by far the most widely-used approach for modeling intracellular processes, ranging from signal transduction pathways to genetic regulatory networks. In contrast intercellular processes, such as for example cell-cell interactions in a tissue, are typically modeled by means of individual cell based models (cellular automata, agent based systems). Unfortunately, many real-life biological problems involve both intra- and inter-cellular processes. As a consequence none of the above-mentioned, well-understood modeling and simulation approaches directly apply. A naïve approach to bridge these two different scales is to equip every individual cell with a personal copy of the intracellular model. Unfortunately, this results in large ODE models which simulation rapidly becomes prohibitively time-consuming.
The objective of the internship is to design and use abstraction methods for ODE models that allow defining simple stochastic automata - or related structures - that capture in an approximate manner the system's dynamics. This simple structure can then be used in place of the original ODE system for efficient tissue simulation. The applicability of the proposed approach will be evaluated on a model of apoptosis in a tissue.
URL sujet détaillé : http://contraintes.inria.fr/~batt/teaching/multiscale.pdf
Remarques :
|
|
|
|
|
|
SM207-8 génération dynamique de code pour microcontrolleurs
|
|
|
Description
|
|
Le contexte de ce stage est la génération dynamique de code, pour lequel le laboratoire développe un outil appelé deGoal. Il s'agit de faire en sorte qu'une application puisse modifier au vol tout une partie de son code, afin de tenir compte du contexte d'exécution et en particulier les données à traiter. Cette technique a été appliquée avec succès dans le domaine du HPC (High Performance Computing -- super-calculateurs massivement parallèles) et du multimédia.
Il existe plusieurs techniques de génération dynamique de code, par exemple : l'interprétation de code (Python, Perl, etc.), et la compilation dynamique aussi appelée JIT compilation (psyco/PyPy pour Python, Java, etc.). Cependant, ces techniques présentent l'un des deux inconvénients suivants : (1) une faible performance d'exécution et/ou (2) une empreinte mémoire importante. Pour ces raisons, il n'est pas possible de générer dynamiquement du code sur des micro-contrôleurs ou des petits processeurs.
Au contraire, avec notre outil deGoal, nous pouvons obtenir des générateurs de code rapides et à très faible empreinte mémoire. L'objectif de ce stage est d'appliquer nos techniques de génération de code aux micro-contrôleurs, et d'étudier une application dans une architecture de réseaux de capteurs.
Objectifs du stage
Le stagiaire devra :
* porter deGoal pour un ou deux micro-contrôleurs utilisés dans les réseaux de capteurs
* faire un état de l'art des classes d'algorithmes et d'applications qui peuvent se prêter à la génération de code au vol dans les applications de réseaux de capteurs
* mettre en oeuvre un démonstrateur
Le stage s'effectuera au sein du laboratoire LIALP du CEA-LIST (Laboratoire Infrastructures et Ateliers pour le Logiciel sur Puces).
Le stage sera rémunéré,
URL sujet détaillé :
:
Remarques : Le stage sera rémunéré
|
|
|
|
|
|
SM207-9 Évaluation de performances pour les systèmes embarqués avec des méthodes formelles
|
|
|
Description
|
|
Le contexte du stage est l'analyse de performance pour les systèmes embarqués. Nous cherchons un compromis entre les méthodes analytiques (modélisation du système puis résolution par des équations mathématiques) et les méthodes à base de simulation, en utilisant les méthodes formelles (interprétation abstraite, model-checking, ...)
URL sujet détaillé : http://www-verimag.imag.fr/Master-2R-2011-2012-Performance.html
Remarques : Co-encadré par Karine Altisen et Matthieu Moy
|
|
|
|
|
|
SM207-10 Techniques de compilation dédiées pour un langage spécifique à un domaine (SystemC)
|
|
|
Description
|
|
SystemC est une bibliothèque utilisée pour la modélisation de haut niveau des systèmes embarqués. Un programme SystemC peut être compilé avec n'importe quel compilateur C++, mais celui-ci manquera beaucoup d'optimisations par manque de connaissance sur la sémantique de SystemC. Nous cherchons à exploiter au maximum les spécificités de SystemC pour écrire un optimiseur plus efficace.
URL sujet détaillé : http://www-verimag.imag.fr/M2R-2012-2013-Dedicated.html
Remarques :
|
|
|
|
|
|
SM207-11 Multithreading sous Matlab
|
|
|
Description
|
|
Matlab est un environnement de calcul et de programmation scientifique très utilisé pour la puissance de son moteur (noyau de traitement constitué de routines optimisées) et sa très grande flexibilité (prise en main aisée et utilisation assez souple). Toutefois, dans sa version "langage de programmation", il propose un interpréteur à la place d'un compilateur. Ceci justifie sa souplesse de programmation et d'exécution interactive, mais en contre partie, il y a d'une part le surcoût sur le temps global d'exécution qui est dû au fonctionnement de l'interpréteur, et d'autre part la difficulté (voire l'impossibilité) d'utiliser directement les outils traditionnels d'analyse et d'optimisation de codes (y compris la parallélisation). Notons toutefois qu'il existe un moyen de se raccrocher à un langage compilé tel que le C (C++ ou Fortran) via le mécanisme des fichiers "mex".
Avec l'avènement des machines multicóurs, il devient indispensable d'offrir la possibilité de paralléliser les applications dans tout environnement de programmation ou de calcul. Le but de ce stage sera donc d'étudier ce problème dans le cadre de Matlab. En résumé, il s'agit d'étudier les mécanismes de programmation ou d'exécution multithreadée sous Matlab, en analyser les avantages et inconvénients, et procéder à des études de cas avec mesures de performances commentées. Ce sera l'occasion pour le stagiaire, en fonction de ses capacités, de développer aussi sa propre méthodologie, tout au moins en initier une qui pourra être approfondie plus tard et étendue aux environnements similaires.
PREREQUIS: Le candidat devra avoir un niveau acceptable en C et connaître un peu Matlab (pas indispensable toutefois, à défaut il y aura une phase de familiarisation préalable). De même, des notions de base de parallélisme sont importantes, surtout le modèle à mémoire partagé. L'occasion sera donnée au candidat de s'initier à la parallélisation automatique.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-12 How to gamble efficiently?
|
|
|
Description
|
|
Betting is an important problem faced by millions of sports fans each day. Presented with an upcoming matchup between team A and team B, and given the opportunity to place a 50/50 wager on either, where should a gambler put her money? This decision is not, of course, made in isolation: both teams will have played a number of decided matches with other teams throughout the season. Furthermore, a reasonable assumption to make is that the relation =93A tends to beat B=94 is transitive. Under transitivity, the best prediction strategy is clearly to sort the teams by their abilities and predict according to this ranking.
The obvious difficulty is that the best ranking of the teams is not known in advance. But there's a more subtle issue: even with knowledge of all match outcomes in advance, i.e. a list of items of the form (team X < team Y ), it's NP-hard to determine the best ranking of the teams when the outcomes are noisy. This is exactly the infamous Minimum Feedback Arc Set problem.
The question we pose is as follows: can we design a non-trivial online prediction strategy in this setting which achieves vanishing regret relative to the best ranking in hindsight, even when the latter is computationally infeasible?
The main goal of this internship is to get acquainted with the recent literature in iterative algorithms for ranking and their application to efficient gambling. This theoretical part will be complemented by an implementation of such algorithms and their evaluation on real data.
References
Near-Optimal Algorithms for Online Matrix Prediction, E. Hazan, S. Kale, S. Shalev-Schwartz, available at http://arxiv.org/abs/1204.0136.
Iterative Ranking form Pair-wise comparisons. S. Negahban, S. Oh and D. Shah
available at http://arxiv.org/abs/1209.1688.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-13 Sketch *-metric
|
|
|
Description
|
|
The interest of estimating distances between several data streams is important in data inten- sive applications. Many different domains are concerned by such analyses including machine learning, data mining, databases, information retrieval, and network monitoring. In all these applications, it is necessary to quickly and precisely process a huge amount of data. For in- stance, in IP network management, the analysis of input streams allows to rapidly detect the presence of anomalies or intrusions when changes in the communication patterns occur. To accurately analyze streams of data, a panel of information-theoretic measures and distances have been proposed to answer the specificities of the analyses. Among them, the most com- monly used are the Kullback-Leibler (KL) divergence, ore more generically, the f -divergences, the Jensen-Shannon divergence and the Battacharyya distance. Unfortunately, computing in- formation theoretic measures of distances in the data stream model is challenging essentially because one needs to process a huge amount of data sequentially, on the fly, and by using very little storage with respect to the size of the stream. In addition the analysis must be robust over time to detect any sudden change in the observed streams (which may be the manifestation of routers deny of service attack or worm propagation). We want to extend [1] to the distributed functional monitoring model [2]. Specifically, the first objective of this master is to propose an enhanced metric that reflects the relationships between any set of discrete probability distributions in the context of massive data streams. This metric should be able to efficiently estimate a broad class of distances measures between large data streams by computing these distances only using compact synopses or sketches of the streams. It should be distribution-free and should make no assumption about the underlying data vol- ume. The second objective is to propose a one-pass distributed algorithm that approximates this novel metric with a given probability δ. This algorithm should use very little space and few operations (i.e., sublinear in the parameters of the system =97 size of the stream, number of distinct items in the streams).
URL sujet détaillé : https://www.dropbox.com/s/24k4t8hpdv0vntp/stage.pdf
Remarques : Co-encadrement avec Emmanuelle Anceaume, projet CIDRE (anceaume.fr), Bruno Sericola, projet DIONYSOS (sericola.fr), à Rennes.
Bio: Yann Busnel is a former student of Ecole Normale Suprieure de Cachan. He is currently an Associate Professor in University of Nantes (France), involved in the Large-Scale Data Management team. He obtained his PhD degree in Computer Science in 2008 from the University of Rennes (France). Then, in 2009, he spent one year as a Researcher at MIDLAB, involved in the distributed systems research group of the University of Rome =93La Sapienza=94 (Italy). He works essentially on very large scale dynamic distributed algorithm and data management in large-scale systems. He also an external reviewer of several international journal and conferences.
|
|
|
|
|
|
SM207-14 Algorithmes distribués pour la planification de centre de soin et de commerces
|
|
|
Description
|
|
D'une manière globale, le travail de l'étudiant est de nature algorithmique et vise à mettre en oeuvre un
prototype logiciel sous environnement linux qui calcule de manière rapide la distance par le réseau
routier entre l'ensemble des foyers suédois et un ensemble de point données et qui par extension
optimise la location de ces points. En pratique, le travail consistera à choisir un algorithme efficace pour
ce calcul, l'implémenter et le tester sachant que le calcul des distances peut réutiliser des valeurs
précédemment calculées. L'algorithme et son implémentation seront distribués (environnement MPI).
Différentes fonctions d'évaluations seront utilisées. L'étudiant disposera des données officielles du
réseau routier suédois, de la population ainsi que du code C pour lire et utiliser ces données.
URL sujet détaillé : http://www.du.se/~prb/Stage.pdf
Remarques :
|
|
|
|
|
|
SM207-15 Compilation and diagnosis for discrete controller synthesis
|
|
|
Description
|
|
Context
Discrete Controller Synthesis (DCS) is a formal method which operates on a non-deterministic program containing controllable variables, and a behavioral property a priori not verified by this program. From this, DCS computes a controller, which, composed with the original program, will enforce the behavioral property on it.
BZR is a reactive language, belonging to the synchronous languages family. It is based on data-flow and automata styles, and its main feature is to include discrete controller synthesis within its compilation. This feature allows to describe programs in an imperative part, which describes possible behaviors, and a declarative part, which specifies behavioral constraints to be respected.
The latter is a behavioral contract mechanisms, where assumptions can be described, as well as an "enforce" property part: the semantics of this latter is that the property should be enforced by controlling the behaviour of the node equipped with the contract. This property will be enforced by an automatically built controller, which will act on free controllable variables given by the programmer.
This Masters will focus on the problem of diagnosis of BZR programs, which is made special by the fact that discrete controller synthesis can find a solution when it exists, but it is not easy to precisely diagnose cases where no solution can be found. This will be studied in relation with related work in declarative and constraints languages, and diagnosis techniques will be defined, and integrated with the imperative aspects in the language.
Expected work
Formalization of a diagnosis methodology, and implementation of this methodology in the BZR compiler.
URL sujet détaillé :
:
Remarques : co-endreur
Gwenaël Delaval (LIG-INRIA)
gwenael.delaval.fr
|
|
|
|
|
|
SM207-16 Energy profiling of networked embedded systems
|
|
|
Description
|
|
Context
Technology clearly evolves towards making communicating sensing digital devices increasingly minia- turized and cheaper to manufacture. Today's platforms are mostly battery-powered, i.e. they benefit from an energy supply that is steady in time but for a globally limited duration. However, embedded energy harvesting will soon become a reality, providing the system quasi-unlimited lifetime but with important unpredictable fluctuations in generated power.
These platforms will remain very difficult to program, in particular because of this energy consumption issue. From the software point of view, application developers will need to build programs that will ensure 1) energy preservation compatible with the desired application lifetime and 2) resistance to power fluctuations imposed by harvesting mechanisms.
The global scope of the project aims at providing extensions to existing low-power operating system infrastructures for supporting energy-efficiency control for very-low-power networked embedded platforms. Eventually, the system designer should be able: 1) to formulate, at different levels in a node's software stack, constraints about energy consumption for each service provided; 2) to define priorities between different concurrent software activities depending on instantaneous availability of power. Beyond this, the application designer should be able to build energy-wise estimation of software solutions to be deployed on a given node and understand how their high-level design choices impact the energy consumption of the application.
Goals
The student will have to design and implement a communicating application on a provided prototyping embedded platform. Then, the first goal of this work is to perform various energy measurements [3] on the platform, in order to characterize the power consumption behaviour of different components [1]. The second goal of this work is to incorporate the obtained energy model directly in the corresponding software components, in order to make the application energy-aware.
URL sujet détaillé : http://perso.citi.insa-lyon.fr/gsalagnac/files/stage-energie.pdf
Remarques :
|
|
|
|
|
|
SM207-17 Model-Checking Techniques for Virus and Malware Detection
|
|
|
Description
|
|
The number of malwares that produced incidents in 2010 is more than 1.5 billion. A malware may bring serious damage, e.g., the worm MyDoom slowed down global internet access by ten percent in 2004. Authorities investigating the 2008 crash of Spanair flight 5022 have discovered a central computer system used to monitor technical problems in the aircraft was infected with malware. Thus, it is crucial to have efficient up-to-date virus detectors. Existing antivirus systems use various detection techniques to identify viruses such as (1) code emulation where the virus is executed in a virtual environnement to get detected; or (2) signature detection, where a signature is a pattern of program code that charaterizes the virus.
A file is declared as a virus if it contains a sequence of binary code instructions that matches
one of the known signatures. Each virus variant has its corresponding signature.
These techniques have some limitations. Indeed, emulation based techniques can only check the program's behavior in a limited time interval.
They cannot check what happens after the timeout. Thus, they might miss the viral behavior if it occurs after this time interval.
As for signature based systems, it is very easy to virus developers to get around them.
It suffices to apply obfuscation techniques to change the structure of the code while keeping the same functionality, so that the new version does not match the known signatures. Obfuscation techniques can consist in inserting dead code, substituting instructions by equivalent ones, etc.
Virus writers update their viruses frequently to make them undetectable by these antivirus systems.
To sidestep these limitations, instead of executing the program or making a syntactic check over it, virus detectors need to use analysis techniques that check the behavior (not the syntax) of the program in a static way, i.e. without executing it. Towards this aim, we propose to use model-checking for virus detection. Model-checking has already been applied for this purpose. However, the existing works have some limitations. Indeed, the specification languages they use have only been applied to specify and detect a particular set of malicious behaviors. They cannot be used to detect all viruses behaviors. Thus, one of the main challenges in malware detection is to come up with specification formalisms and detection techniques that are able to specify and
detect a larger set of viruses.
The purpose of this internship is to (1) define expressive logics that can be used to compactly express malicious behaviors. Our goal is to be able to express malicious behaviors that were not considered in the litterature. (2) Define efficient model-checking algorithms for these logics. (3) Reduce the malware detection problem to the model-checking problem of these logics. And (4) define interesting program abstractions that would make these techniques applicable to large programs.
URL sujet détaillé : www.liafa.univ-paris-diderot.fr/~touili/sujet-master.pdf
:
Remarques :
|
|
|
|
|
|
SM207-18 Calcul d'index pour le problème du logarithme discret sur courbes elliptiques
|
|
|
Description
|
|
Le problème du logarithme discret sur courbes elliptiques est un des problèmes les plus importants en cryptographie. Après vingt ans de cryptanalyse infructueuse, ce problème semble beaucoup plus difficile à résoudre que les deux autres problèmes très utilisés en cryptographie (le problème de la factorisation d'entiers et le problème du logarithme discret sur les corps finis). Récemment, la méthode du calcul d'index (qui a mené aux meilleurs algorithmes pour les deux autres problèmes) a pu progressivement être adaptée aux courbes elliptiques sur des corps de petite caractéristique.
Le stage fera le point sur les résultats récents de Diem, Faugère, Gaudry, Hodges, Joux, Perret, Petit, Renault, Semaev, Schlaffer, Vitse. Il proposera des variantes des attaques existentes et réalisera des implémentations en Magma.
URL sujet détaillé :
:
Remarques : Christophe Petit, chargé de recherches à l'UCL Crypto Group, assurera l'encadrement au quotidien.
|
|
|
|
|
|
SM207-19 Le Rubik's cube pour les cryptographes
|
|
|
Description
|
|
Il est bien connu que l'ensemble des configurations du Rubik's cube forme un groupe fini qui peut être engendré par les 6 permutations élémentaires. Ce casse-tête bien connu est réputé difficile, mais certainement pas au sens cryptographique du terme. Il existe en effet des algorithmes très efficaces pour résoudre le Rubik's cube, le record du monde pour un être humain étant de seulement 7,08 secondes.
La sécurité d'un très grand nombre de protocoles cryptographiques utilisés quotidiennement, comme le RSA, repose sur l'hypothèse que certains problèmes mathématiques sont très difficiles à résoudre, même avec l'aide d'ordinateurs très puissants. Les problèmes les plus célèbres utilisés en cryptographie sont la factorisation entière (utilisée dans le cas du RSA) et le logarithme discret, mais d'autres problèmes moins connus ont également été proposés, et pourraient (qui sait?) peut-être les remplacer un jour.
Ce mémoire s'intéresse aux problèmes de représentation et de factorisation dans des groupes finis non commutatifs. Le problème de représentation est le suivant: étant donné un groupe fini G et un ensemble d'élements s_i appartenant à G qui génèrent le groupe, trouver une combinaison des éléments s_i qui se ramène à l'élément neutre du groupe. Le problème de factorisation est un peu plus général: on reçoit en plus un élément quelconque du groupe, et on doit trouver une combinaison des éléments s_i qui se ramène à cet élément.
Pour fixer les idées, on peut reprendre l'exemple du Rubik's cube. Dans ce cas, le groupe G est l'ensemble des permutations possibles du cube. L'élément neutre correspond à la configuration de base. Si les éléments s_i choisis sont les permutations élémentaires (les 6 rotations d'un quart de tour), alors on sait que le problème de représentation est facile à résoudre. Le problème de factorisation est beaucoup moins étudié (et ne fait pas encore partie des épreuves des championnats du monde!) mais n'est probablement pas beaucoup plus compliqué.
Pour revenir à la cryptographie, plusieurs fonctions de hachage (une des primitives les plus utilisées en cryptographie) ont été proposées, dont la sécurité repose sur la difficulté de résoudre les problèmes de représentation et de factorisation dans des groupes de matrices 2*2 à coefficients dans un corps fini. Dans ce cas, le problème de représentation sera le suivant: on reçoit deux matrices A et B qui génèrent le groupe, et il faut trouver un produit de ces matrices (le plus petit possible) qui donne la matrice identité. Plusieurs des schémas proposés ont été cassés, complètement ou en partie, mais d'autres schémas continuent de défier la communauté scientifique.
Le stage fera le point sur les attaques connues, proposera des améliorations ou extensions, et implémentera les résultats en Magma.
URL sujet détaillé :
:
Remarques : Christophe Petit, chargé de recherches à l'UCL Crypto Group, assurera l'encadrement au quotidien.
|
|
|
|
|
|
SM207-20 Anonymous blacklisting without trusted third party
|
|
|
Description
|
|
There are many systems allowing to communicate privately over the internet. Tor (https://www.torproject.org/) being the most famous. The problem with such anonymizing networks is that there is no easy way to establish accountability of anonymous users. Therefore many services, web site administrators, block all known exit nodes of anonymizing networks since they can't rely on IP-adresses of misbehaving clients. In the end it challenges the success of anonymizing networks.
Some solutions have been presented in order to block misbehaving users while keeping their anonymity protected. Anonymous blacklisting is a very alive research field.
The aim of the internship is first to make a state-of-the art survey of this field. A second aim would be to develop a system allowing blacklisting while maintaining anonymity in a completely decentralised manner, for instance by re-using ideas developped for distributed electronic cash à la Bitcoin (http://bitcoin.org/).
Don't hesitate to contact me for more informations.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-21 Dynamic non-interference
|
|
|
Description
|
|
Noninterference is the mathematical basis for confidentiality
analyses. The problem is simple: how to shape and control the
information flow in such a way that data labeled private cannot be
publically observed ? The noninterference approach is intuitive: data
are tagged with security level and it aims at proving that
modifications of a data tagged ``high'' cannot lead to modifications
of data tagged ``low''. The system has to enforce
noninterference. Historically it was first done dynamically. In order
to enhance performances and also to keep track of implicit flows
followed static based systems, for instance through the use of
suitable type systems starting with the work of Smith Volpano and
Irvine and leading to many systems.
Though intellectualy seducing noninterference approaches have often
been shown as rather unrealistic. Indeed basic scenarios like password
checking or even cryptogaphy, which conceptually is nothing less than
a method explicitely designed to publish private data publically
without compromising confidentiality, are telling. In all those
scenarios noninterference is, from a strict point of view, broken.
Recently, we have proposed a framework allowing to declare security
policies in form of a rewriting system. The idea was to be more
precise than security-typed languages for trusted declassification
functions. Indeed, for each function we do not simply attach a
security type but we provide a set of rewrite rules describing the
security behavior of that function. Moreover we have extended this
work by allowing the security policy to evolve dynamically during
computation.
The aim of this master is to deepens the results on dynamic
interference policies. There are several paths to consider:
1) the framework was designed for a simple imperative language, what happens
if we add non-determinism, concurrency aspects ?
2) a checking algorithm has been proposed but it is a very naive algorithm,
can it be optimised ?
3) is it possible to integrate notions of partial information flows (like
leaking half of a secret) ?
etc.
Don't hesitate to contact me for more informations.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-22 Etude et développement de back-ends LLVM pour les cóurs de traitement hétérogènes d'un circuit télécom, en vue de la mise en place d'une plateforme de radio logicielle (SDR).
|
|
|
Description
|
|
Cadre du stage :
Le laboratoire de circuits numériques du LETI développe depuis plusieurs années des architectures
multi-coeurs comprenant plus de 20 coeurs de calcul organisés autour d'un réseau-sur-puce (NoC). Ces
développements ont été concrétisés dans plusieurs circuits applicatifs, notamment dédiés à des applications
de télécommunication 4G.
Une collaboration avec le laboratoire CITI (Centre d'Innovation en Télécommunications et Intégration de
services), situé sur le campus de l'INSA de Lyon, vise à étudier les problématiques de la radio logicielle :
comment décrire un standard télécom (ou "forme d'onde") sous la forme d'un "programme informatique"
indépendant d'une plateforme matérielle, et comment "traduire" (i.e. compiler) ce programme en un code
performant exécutable sur une plateforme donnée.
Travail demandé :
Ce stage propose l'étude et le développement de back-ends pour le compilateur LLVM, dédiés à chacun des
différents blocs de traitement d'un circuit télécom. Un front-end actuellement développé par un doctorant se
chargera de fournir une représentation intermédiaire du programme de la forme d'onde. Les back-ends
devront traduire des sous parties de cette représentation en binaires exploitables par le matériel, par exemple
du code exécutable sur un CPU ou un DSP, ou des valeurs de configuration pour piloter des blocs matériels
non programmables. Une forte interaction avec le doctorant sera nécessaire pour aboutir à une interface
front-end/back-end pertinente.
Informatique
URL sujet détaillé : http://www.cea.fr/ressources_humaines/stages_et_formation_en_alternance/les_offres_de_stage/liste_des_stages/etude_et_developpement_de_back-ends_llvm_pour_le
Remarques :
|
|
|
|
|
|
SM207-23 Optimisation robustes de réseaux radio d'accès à faisceaux hertziens ou micro-ondes
|
|
|
Description
|
|
Les technologies des réseaux radio à faisceaux hertziens ou micro-ondes (wireless backhaul networks) sont une alternative viable pour apporter l'internet à haut débit dans les " zones blanches ", ainsi que pour le déploiement de réseaux d'opérateurs privés ou de collectivités territoriales en zones urbaines. Ces réseaux utilisent des liens radios directionnels pour transporter des informations à hauts débits sur de longues distances. Or, la capacité d'un lien (micro-ondes) d'un réseau d'accès sans fil dépend des conditions environnementales et sera réduite en cas de pluie ou de changement important de la température (incendie, canicule). Comme la pluie affecte en général plusieurs liens simultanément, on peut associer une certaine probabilité dépendant des conditions environnementales aux capacités de certains ensembles de liens et étudier dans ce modèle des problèmes d'optimisation comme le routage. L'objectif est donc de développer des modèles permettant de résoudre des problèmes complexes liés à la conception et au déploiement de réseaux radio d'accès en prenant en compte les variations environnementales et de trafic de ces réseaux.
Les objectifs visés sont :
1.Proposer un cadre théorique pour modéliser les effets des variations de trafic et les ensembles de liens sujets à une baisse de capacité dans ce type de réseaux.
2.Développer des modèles d'optimisation efficaces utilisant l'optimisation robuste, stochastique, ou " chance-constrained ".
3.Proposer des outils de conception de réseaux et de leur fonctionnement dans ces contextes, en particulier pour la conception de réseaux robustes aux variations de trafic et de capacités.
URL sujet détaillé : http://www-sop.inria.fr/members/Christelle.Molle-Caillouet/InternRobust.pdf
Remarques : Lieu de travail :
INRIA Sophia-Antipolis Méditerranée
Equipe MASCOTTE (http://www-sop.inria.fr/mascotte/)
Email des personnes à contacter (les porteurs du sujets) :
christelle.caillouet.fr
david.coudert.fr
|
|
|
|
|
|
SM207-24 Energy efficient point coverage problem using UAVs
|
|
|
Description
|
|
Recent advances of technology have led to the development of flying drones that can be used to track objects lying on the ground. During the last years, an increased use of flying drones has been noticed. The invention of light materials, low energy consumption machines and high performance small processing units led to the construction of flexible flying robots. This kind of robots (also called Unmanned Aerial Vehicles or UAVs) can be used in a variety of applications such as vehicle tracking, traffic management and fire detection. They are able to fly autonomously in different altitudes and they are usually equipped with sensor units to monitor the environment and communication units to exchange data with other drones or central stations.
This project aims at filling the gap with existing work and actual requirements regarding the deployment of UAVs. More specifically we want to develop a set of models and algorithms that could provide an efficient and reliable drone placement and scheduling by adjusting the drones position ensuring the surveillance of all the targets at the same time. This problem is related to the set covering problem, and more precisely a study of its dynamic version has to be done when starting the project.
The following characteristics are of specific interest:
- Quality: A minimum coverage quality of the events should be kept
- Communication between drones should be optimize for data gathering from drone to central station
- Energy consumption should be minimized at each drone and/or at the network level
- Scalability is an important feature since deployment area and number of events are not known a priori
- Robustness: Communication failure should not alter the coverage quality and classic operation or at least its effect should be minimized.
URL sujet détaillé : http://www-sop.inria.fr/members/Christelle.Molle-Caillouet/InternUAVs.pdf
Remarques : Lieu de travail :
INRIA Sophia-Antipolis Méditerranée,
Equipe MASCOTTE (http://www-sop.inria.fr/mascotte/)
|
|
|
|
|
|
SM207-25 Analyse et inférence géométrie de formes 3D par diagramme d'épaisseur
|
|
|
Description
|
|
Dans de nombreuses applications d'analyse ou de modélisation de forme, il est parfois crucial de bénéficier d'une information locale d'épaisseur. Parmi les différentes solutions existantes, la fonction d'épaisseur que nous utilisons associe à chaque point d'une forme, le rayon de la plus grosse boule interne contenant ce point. Cette fonction est pertinente pour de nombreuses raisons : elle est définie de manière volumique (en tout point de l'espace), elle possède de bonne propriétés d'inférence géométrique (convergence des mesures lors d'une approximation de plus en plus fine d'un objet continu). Enfin, dans le cas discret, cette fonction permet de construire une structure combinatoire, appelée diagramme d'épaisseur, intéressante d'un point de vue algorithmique. Appliquées à des objets digitaux (région dans une image) ou des approximations par nuage de points d'un objet continu, nous avons obtenu plusieurs résultats théoriques et expérimentaux préliminaires sur ces notions.
L'objectif du stage est de s'intéresser à une analyse et à une implémentation exacte du diagramme d'épaisseur dans le cas 3D en se basant sur des outils de géométrie algorithmique. Par ailleurs, nous nous intéresserons à l'utilisation de ce diagramme pour de la caractérisation de formes.
Ce stage se déroulera au sein des équipes geomod et m2disco du LIRIS.
URL sujet détaillé :
:
Remarques : * Co-encadrement avec Raphaelle Chaine (MCF, LIRIS, Geomod)
* Stage avec indémnisation
|
|
|
|
|
|
SM207-26 Cycles de partage dans les triangulations
|
|
|
Description
|
|
L'étude des cycles d'un graphe plongé dans une surface topologique, en concomitance avec certaines propriétés topologiques, a reçu une attention particulière dans les deux dernières décennies.
Un problème ouvert concerne le calcul d'un cycle de partage. Soit G un graphe plongé dans une surface S. Un cycle de partage est un cycle de G qui coupe S en deux composantes non triviales,
c'est-à-dire non homéomorphes à un disque. Décider si G possède un cycle de partage est NP-complet. Cependant, si G triangule S, =16 i.e. G découpe S en triangles, =16 Barnette (1982) a conjecturé que G possède toujours un cycle de partage. L'objet de ce stage est d'étudier cette conjecture. Une approche expérimentale semble confi=1Crmer la conjecture lorsque S est un double tore (genre 2). Le candidat pourra commencer par s'intéresser à la conjecture pour le genre 2.
URL sujet détaillé : http://www.gipsa-lab.fr/~francis.lazarus/Stages/stageENSLyon13-a.pdf
Remarques : rémunération forfaitaire.
|
|
|
|
|
|
SM207-27 Aspects dynamiques de l'algorithmique des surfaces combinatoires
|
|
|
Description
|
|
Une surface combinatoire est une décomposition en faces, arêtes et sommets d'une surface topologique (une variété compacte de dimension deux). Les notions classiques d'homotopie et d'homologie relatives aux courbes tracées sur une surface s'expriment dans un cadre combinatoire pour les chemins tracés dans le graphe sommets-arêtes d'une surface combinatoire.
Les aspects algorithmiques en lien avec l'homotopie et l'homologie ont reçu une attention particulière dans les deux dernières décennies.
L'objectif du stage est de revisiter ces résultats dans un cadre dynamique où la surface combinatoire est modi=1Cfiée par des opérations élémentaires comme la contraction ou la suppression d'arêtes. On pourra s'intéresser dans un premier temps à des questions simples portant sur l'existence de courbes ayant certaines propriétés topologiques (contractibles, séparatrices,. . .).
URL sujet détaillé : http://www.gipsa-lab.fr/~francis.lazarus/Stages/stageENSLyon13-b.pdf
Remarques : rémunération forfaitaire.
|
|
|
|
|
|
SM207-28 Reconstruction d'images par méthodes proximales rapides d'optimisation convexe
|
|
|
Description
|
|
Ce stage vise à étudier la vitesse de convergence et à accélérer des méthodes itératives récentes d'optimisation convexe non lisse par éclatement (splitting). La validation se fera sur des problèmes inverses classiques de traitement d'image.
Voir le .PDF pour un descripptif détaillé.
Ask me if you want the description in English.
URL sujet détaillé : www.gipsa-lab.fr/~laurent.condat/download/stage1.pdf
:
Remarques : La volonté de l'étudiant de poursuivre en thèse ce sujet ambitieux est désirée.
|
|
|
|
|
|
SM207-29 Phénomènes de diffusion dans les réseaux
|
|
|
Description
|
|
La propagation des épidémies, des rumeurs, des virus informatiques, ou la diffusion d'une information sont des exemples types de phénomènes de diffusion. De par leur importance, ces phénomènes sont au cóur d'une intense activité de recherche.
Il est toutefois extrêmement difficile d'avoir une information précise sur comment des processus de diffusion réels se passent : il faut connaître le réseau entre les acteurs, les changements d'états
et leurs causes, tout ceci au cours du temps et à une échelle suffisament grande pour permettre l'analyse. Aujourd'hui, les données de ce type sont extrêmement rares, et souvent très partielles et biaisées.
Par conséquent, à quelques exceptions près, la plupart des travaux concernant les phénomènes de diffusion reposent sur des modèles, qui eux-mêmes reposent sur des intuitions simples (par exemple l'idée selon laquelle une personne infectée aurait une certaine probabilité de contaminer ses contacts).
L'équipe Complex Networks du LIP6 est impliquée depuis plusieurs années dans la collecte de données riches et à large échelle, dont certaines permettent d'ouvrir des perspectives extrêmement prometteuses pour l'analyse de phénomènes de diffusion réels, et donc leur modélisation.
Le stage proposé ici vise à utiliser ces données pour obtenir, pour la première fois, des observations quantitatives sur des phénomènes de diffusion réels. L'objectif central est de confronter ces mesures aux modèles existants et ainsi d'évaluer la pertience des hypothèses sous-jacentes. On dégagera ainsi de grands principes, confrontés à la réalité, pour la modélisation des phénomènes de diffusion.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2010/11/diffusion1.pdf
Remarques :
|
|
|
|
|
|
SM207-30 Modélisation robuste et intuitive d'objets 3D hautement complexes
|
|
|
Description
|
|
Les univers virtuels sont devenus des éléments incontournables de notre environnement quotidien. On les retrouve systématiquement dans les programmes télévisés, les jeux, les films d'animation, la simulation, la construction (aéronautique, navale, automobile), l'urbanisme, etc. La création numérique de ces environnements passe par la création des objets tridimensionnels qui les composent.
Depuis maintenant un peu plus de dix ans, les imprimantes 3D se développent. De nos jours, les plus petites et moins onéreuses coûtent autour de 400 euros et les plus évoluées permettent d'imprimer des objets de grande taille dans des matériaux diverses comme le plastique, la céramique, les méteaux, le verre, etc. A la vue de cette évolution, on peut facilement imaginer le développement d'un marcher via le web, puis, peut-être un jour, directement chez les particuliers. L'enjeu est ici très important car il s'agit de donner l'accé à la fabrication à tous. Il y a ici le potentiel d'une vraie révolution. La modélisation géométrique de formes 3D est dans ce cas l'outil qui permet à l'utilisateur de s'interfacer avec l'imprimante.
De nos jours, l'utilisation de logiciels de création d'objets tridimensionnels complexes reste réservée à des utilisateurs experts. Le but de se stage est, dans un premier temps, d'étudier l'état de l'art des techniques de création intuitives d'objets tridimensionnels. Dans un deuxième temps, l'objectif est de proposer un modèle de représantation de surface adapté à la représentation de surfaces très complexes, contrôlables de façon intuitive et précise par un utilisateur non expert. L'aspect robustesse et simplicité de développement informatique sera aussi à prendre en compte.
URL sujet détaillé : http://www.irit.fr/~Loic.Barthe/Tmp/ENS-Stage/
Remarques : A voir directement avec l'encadrant.
|
|
|
|
|
|
SM207-31 Simplification Topologique de Champs Scalaires Volumiques
|
|
|
Description
|
|
Contexte Général :
=Les champs scalaires (fonctions réelles définies sur des variétés) sont des données très récurrentes en Visualisation Scientifique, par exemple dans le contexte d'analyse de simulations physiques ou d'acquisition volumique. Pour appréhender la complexité de ces données, de nombreuses techniques topologiques issues de la théorie de Morse [1] ont été proposées pour capturer la structure du champ (les relations entre ses singularités) dans des abstractions topologiques de haut niveau comme les graphes de Reeb [2, 3] ou les complexes de Morse-Smale [4]. De plus, des méthodes efficaces existent pour la simplification de ces abstractions [5, 6], produisant ainsi des représentations multi-échelles de la topologie du champ. Cependant, ces dernières méthodes ne simplifient pas le champ scalaire sous-jacent directement. Or, dans de nombreuses applications, il peut être utile de simplifier le champ, ne serait-ce que pour visualiser l'impact de la simplification. Par ailleurs, la simplification de la topologie du champs en tant que pré-traitement permet d'accélérer grandement la plupart des algorithmes topologiques, rendant ainsi possible l'analyse topologique dans un contexte de visualisation in-situ (en même temps que la simulation produisant la donnée).
Objectifs du stage :
=Dans ce stage, nous souhaiterions développer de nouveaux algorithmes pour la simplification topologique de champs scalaires définis sur des 3 variétés linéaires par morceaux (maillages tétraédriques). Par contraste avec les approches numériques (visant à approcher la solution par résolution d'équations aux dérivées partielles), nous souhaiterions développer un algorithme combinatoire, ce type d'approche permettant de fournir des garanties topologiques fortes sur la justesse du résultat au travers de preuves formelles.
Plusieurs algorithmes combinatoires ont été proposés dans le cas des champs scalaires définis sur des 2-variétés [7, 8, 9] dont un récemment, plus général que les approches précédentes, par l'un des encadrants de ce sujet de stage [10] (Fig. 1). Cependant, en augmentant la dimension du domaine (en passant des surfaces aux volumes), le problème devient notoirement plus compliqué, puisque de nouveaux types de singularités émergent dans les champs au fur et à mesure que la dimension augmente. Le stage pourra se décliner selon les étapes suivantes :
1. Étude bibliographique (cf Références bibliographiques ci-dessous)
2. Étude des avantages et inconvénients des différents formalismes de représentation et de manipulation des champs scalaires (réprésentations linéaires par morceaux traditionnelles ou par gradient discret [11, 12]).
3. Extension directe de l'algorithme présenté dans [10] pour la suppression des paires de singularités extrema/selles.
4. Définition d'un nouvel algorithme pour la suppression des paires de singularités 1-selles/2-selles.
5. Implémentation de l'algorithme.
Selon l'avancement du stagiaire, de nombreuses applications en Visualisation Scientifique pourront être mises en óuvre, notamment pour la simplification de rendus volumiques guidés par la topologie. Enfin, selon l'avancement du stagiaire, la publication des résultats de ce stage est envisagée.
Compétences espérées
=Des connaissances rudimentaires en géométrie algorithmique sont nécessaires. Des compétences en C ou C++ constituent un plus. Curiosité, persistance et aptitudes au travail d'équipe sont des compétences humaines bienvenues !
Questions/Contacts
=N'hésitez pas à contacter Julien Tierny ou Pooran Memari en cas de question.
Références bibliographiques
=[1] Morse M., " Relations between the critical points of a real function of n independant variables ", Transactions of the American Mathematical Society, 1925.
[2] Reeb G., " Sur les points singuliers d'une forme de Pfaff complètement intégrable ou d'une fonction numérique ", Comptes-rendus des Séances de l'Académie des Sciences, 1946.
[3] Tierny J., Gyulassy A., Simon E., Pascucci V., " Loop Surgery for Volumetric Meshes : Reeb Graphs Reduced to Contour Trees ", IEEE Transactions on Visualization and Computer Graphics (Proc. Of IEEE VIS 2009).
[4] Gyulassy A., Bremer P.T., Hamann B., Pascucci V., " A practical approach to Morse-Smale Complex Computation : Scalability and Generality ", IEEE Transactions on Visualization and Computer Graphics (Proc. Of IEEE VIS 2008).
[5] Edelsbrunner H., Letscher D., Zomorodian A., " Topological Persistence and Simplification ", Discrete and Computational Geometry, 2002
[6] Carr H., Snoeyink J., Ulrike A., " Simplifying flexible isosurfaces using local geometrical measures ", Proc. Of IEEE VIS 2004.
[7] Edelsbrunner H., Morozov D., Pascucci V., " Persistence-sensitive simplification of functions on 2-manifolds ", Proc. Of ACM Symposium on Computational Geometry, 2006.
[8] Attali D., Glisse M., Hornus S., Lazarus F., Morozov D., " Persistence-sensitive simplification of functions on surfaces in linear time ", Proc. Of TopoInVis 2009.
[9] Bauer U., Lange C., Wardetzky M., " Optimal topological simplification of discrete functions on surfaces ", Discrete and Computational Geometry, 2012.
[10] Tierny J. and Pascucci V., " Generalized Topological Simplification of Scalar Fields on Surfaces ", IEEE Transactions on Visualization and Computer Graphics (Proc. Of IEEE VIS 2012).
[11] Forman R., " A User's Guide to Discrete Morse Theory ", Advances in Mathematics, 1998.
[12] Gunther D., Reininghaus J., Prohaska S., Weinkauf T., Hege H.C., " Efficient Computation of a Hierarchy of Discrete 3D Gradient Vector Fields ", Proc. Of TopoInVis 2011.
URL sujet détaillé : http://www.telecom-paristech.fr/~tierny/stuff/openPositions/sujetMasterRecherche.pdf
Remarques : Possibilités de rémunération et de poursuite en thèse.
|
|
|
|
|
|
SM207-32 Shape meshing in high dimensions
|
|
|
Description
|
|
Context.
In many practical situations, the object of study is only known through a finite set of possibly noisy sample points. Given as input these sample points, it is then desirable to reconstruct a model of the object which is both geometrically accurate and topologically correct. The resulting model may then be measured or used for certain tasks such as rendering, storing, searching in a data base and so on. The most obvious example is probably surface reconstruction, where the points are measured on the surface of a real world object. Surface reconstruction from 3D scans has many applications in reverse engineering, biology, medicine, art history. In all these fields, it is necessary to digitize quickly 3D shapes (mechanical pieces, organs, statues and so on).
In other applications, the shape of interest may live in a higher dimensional space, as for instance in machine learning. It should be noted that higher-dimensional point sets found in real applications are often distributed on lower-dimensional surfaces within the ambient space, usually because the number of degrees of freedom of the process generating the points is lower than the dimension of the points generated.
Objectives.
Only recently, some effort has been put into tackling the challenge of high dimensions. A very simple reconstruction method consists in connecting two points in the cloud if the two points are within distance r and then adding a triangle if the three edges are already there, a tetrahedron if the six edges are already there and so on. The result is called the Rips complex of the point cloud with scale parameter r. Rips complexes enjoy the nice property to be completely determined by the graph of their vertices and edges. This compressed form of storage makes Rips complexes very appealing for computations in high dimensions.
Unfortunately, Rips complexes are generally high-dimensional objects and the goal of this project is to propose strategies to simplify them so as to build a model with the correct intrinsic dimension. So far, we tried to simplify the complex by iteratively contracting edges. But the order in which to apply edge contractions still remains unclear. In this project, we would like to investigate other strategies, formalizing the simplification problem as minimizing some energy. For instance, one could imagine throwing a small amount of particles on the complex and then simulate particle repulsion. Based on the way they interact, can we deduce a mesh with the correct intrinsic dimension? A different approach proposed recently is based on the optimal cost to transport the point cloud to a low-dimensional triangulation. Other strategies could be imagined as well ...
URL sujet détaillé : http://www.gipsa-lab.fr/~dominique.attali/Internships/shape-meshing.pdf
Remarques :
|
|
|
|
|
|
SM207-33 Domaines abstraits pour l'analyse de programmes avec mémoire dynamique
|
|
|
Description
|
|
Reasoning about behaviors of programs that manipulate dynamic data structures is a challenging problem because of the difficulty of representing (potentially infinite) sets of configurations, and of manipulating these representations for the analysis of the execution of program statements.
Recent works propose solutions for the analysis of such programs based on abstract interpretation and shape analysis. They use abstract representations of the heap based on graphs or automata which give the shape of the heap. The data stored in the heap is embedded as a labelling of the nodes/states by interpreted predicates or abstract values over data or data sequences. These approaches are very efficient in practice, but they are still limited to simple data structures like singly linked lists or arrays.
This internship has as goal to extend the principle of the abstract domains for singly linked lists with data to more complex structures, e.g., nested lists, hash tables with infinite data in nodes. Moreover, this extension has to be able to deal uniformly with such data structures, thus providing a general interface for the implementation/use of the abstract domains for the graph and for the embeddings of data in the graph. The development of these abstract domain shall be performed together with a study of their use for the verification of program properties involving shape and data constraints.
URL sujet détaillé : http://www.liafa.univ-paris-diderot.fr/~sighirea/uprojects/M2R.adom-heap.pdf
Remarques : Co-encadrement avec Constantin Enea. Possibilité de réservation par l'université d'un logement dans résidences pour étudiants.
|
|
|
|
|
|
SM207-34 Compression de maillages 3D volumiques
|
|
|
Description
|
|
Titre: Compression de maillages 3D volumiques
Ce stage est proposé en collaboration avec IFP Energies nouvelles (IFPEN).
L'utilisation des données 3D est aujourd'hui bien établie dans de nombreuses applications industrielles telles que la visualisation et la simulation scientifique notamment dans le domaine de l'exploration et de la production dans l'industrie Oil&Gas. Les besoins croissants de précision et de qualité dans le domaine de la simulation scientifique ont conduit à une augmentation très importante de la complexité des données 3D produites. Parallèlement ces données sont de plus en plus utilisées dans le cadre d'applications web et de plateformes collaboratives ; elles nécessitent donc d'être transmises rapidement sur le réseau. Ainsi, la compression de ces contenus devient un enjeu scientifique essentiel avec plusieurs objectifs tels que le stockage compact de ces données, une transmission en temps interactif sur le réseau, une visualisation progressive du contenu qui doit être adaptée aux terminaux ou encore un accès aléatoire et rapide.
L'objectif de ce stage est de proposer de nouvelles méthodes de compression de maillages volumiques éventuellement capables de gérer des propriétés attachées, tout en permettant une décompression adaptée aux terminaux de visualisation. Ces données 3D étant issues de calculs scientifiques réalisés au sein de l'IFP Energies nouvelles.
Les algorithmes de compression pour les géométries volumiques permettraient de les exploiter dans les outils logiciels qui manipulent des maillages 3D volumineux (simulation d'écoulement poreux en géosciences ou simulation de combustion en transport). A terme, ils ont vocation à éliminer le verrou technologique concernant les très gros volumes de données avec une cible fixée sur le milliard de mailles. Les résultats seront notamment exploités pour assurer le stockage, le transfert mais aussi la manipulation (exploration, visualisation, filtrage, analyse) de ces très gros volumes de données 3D.
Les travaux s'appuieront sur des travaux récents sur la compression de maillages volumiques [3] ainsi que sur les compétences de l'équipe M2DisCo (http://liris.cnrs.fr/m2disco) du laboratoire LIRIS en termes de compression et notamment les travaux de compression de maillages surfaciques avec des données associées [1, 2, 4] qui utilisent des structures multi-résolution autorisant une décompression progressive. Ainsi, à très bas débit, ces algorithmes sont capables de préserver la forme globale de la géométrie complète, ainsi que l'aspect des données associées.
Bibliographie :
1. Ho Lee, Guillaume Lavoué, Florent Dupont: Rate-distortion optimization for progressive compression of 3D mesh with color attributes. The Visual Computer 28(2): 137-153, 2012.
2. Ho Lee, Çagatay Dikici, Guillaume Lavoué, Florent Dupont: Joint reversible watermarking and progressive compression of 3D meshes. The Visual Computer 27(6-8): 781-792, 2011.
3. Courbet, Clement; Isenburg, Martin, Streaming compression of hexahedral meshes, The Visual Computer, 26(6)/ 1113-1122, 2010.
4. Ho Lee, Guillaume Lavoué, Florent Dupont: Adaptive Coarse-to-Fine Quantization for Optimizing Rate-distortion of Progressive Mesh Compression. VMV 2009: 73-82.
URL sujet détaillé :
:
Remarques : Florence Denis (LIRIS, Université Lyon 1),
Florent Dupont (LIRIS , Université Lyon 1), Guillaume Lavoué (LIRIS, INSA-Lyon),
Sébastien Schneider (IFPEN).
|
|
|
|
|
|
SM207-35 Complexité de communication et langages d'images
|
|
|
Description
|
|
Le but du stage est d'appliquer des méthodes de complexité de communication pour mieux cerner les langages d'images en 2D. Les langages d'images sont une généralisation en 2D du concept de langage rationnel, où la notion de mot est remplacée par la notion d'image (finie). Cependant, à cause de l'indécidabilité de la pavabilité du plan, la plupart des problèmes naturels deviennent indécidables pour les langages d'images. Les approches par automates, par expressions régulières, ne sont plus adaptées et il est nécessaire d'introduire des nouveaux outils.
On cherchera dans le stage à montrer que des méthodes de complexité de communication permettent (dans certains cas!) de résoudre complètement le problème.
Voir le sujet détaillé (ou l'encadrant) pour plus de renseignements.
URL sujet détaillé : http://www.loria.fr/~ejeandel/files/stage-M2.2.pdf
Remarques : Possibilité de continuer en thèse.
|
|
|
|
|
|
SM207-36 Cost models for caching strategies in the cloud
|
|
|
Description
|
|
Context
Cloud computing aims to tackle increasing needs of computing and storage resources, in a user-friendly manner. As a consequence, it has recently attracted an increasing interest, in particular by major IT companies such as Google, Microsoft, Amazon or Facebook. Clouds enable to envision data management at an unexpected scale in various contexts (medical imagery, particles physics, cultural heritage). However, performance of these systems usually relies on brute force (i.e. using more numerous and/or powerful nodes) resulting in high cost and suboptimal resource management.
Performance optimization in databases has been studied for years, in particular using methods such as indexing, materialized views or caching. These methods would help improve the performance in the cloud, optimizing resources management. In particular, semantic caches enable to rewrite queries so that to reuse local results from previous requests. Unfortunately, existing solutions are not suited to cloud data management systems. Indeed, computing a query in a semantic cache may lead to worse response times than using a massively parallel evaluation on, expensively billed, servers.
The proposed project will pursue two main research lines: (1) cost models for semantic caches the cloud and (2) validation in large-scale systems.
Objectives
Semantic caching is a well-known technique to optimize the performance of DBMSs. It enables storing relevant query results and reuses them to save servers' CPU.
The first step of this work consists in proposing a cost model for data management in the cloud, taking into account the pricing model of the main providers such as Amazon, Microsoft and Google and extending it with their specificities (licences, internal data transfers, etc.).
Then, existing semantic will be extended so that to fit cloud computing, in particular relying on multi-criteria optimization. Indeed, current solutions are mainly oriented toward response time's reduction by minimizing the load on servers. Nevertheless, elasticity in cloud computing provides virtually infinite CPU capabilities. In such a context, parameters such as client capability to consume results and user budget have to be fully integrated in the decision process.
Finally, the proposals will be validated thanks to analytical models, simulations and above all experiments. Experiments will be conducted using several infrastructures, in particular the private cloud of Blaise Pascal University, Grid'5000, Microsoft or Amazon.
Plan
Objectives to be achieved are the following:
1. Cost models for data management in a pay-as-you-go context,
2. Cost models for semantic caching to be deployed in elastic environments,
3. Algorithms for cache miss resolution in the cloud and
4. Validation of the proposals on various infrastructures.
References
1. M. Armbrust, A. Fox, R. Griffith, A. D. Joseph, R. H. Katz, A. Konwinski, G. Lee, D. A. Patterson, A. Rabkin, I. Stoica, and M. Zaharia. A view of cloud computing., Communications of the ACM, 53(4):50=9658, 2010.
2. K. S. Beyer, V. Ercegovac, R. Gemulla, A. Balmin, M. Y. Eltabakh, C.-C. Kanne, F. =D6zcan, E. J. Shekita: Jaql: A Scripting Language for Large Scale Semistructured Data Analysis. PVLDB 4(11): 1272-1283, 2011.
3. R. Chaiken, B. Jenkins, P.-=B0A. Larson, B. Ramsey, D. Shakib, S. Weaver, and, J. Zhou. Scope: easy and efficient parallel processing of massive data sets. Pro-, ceedings of the Very Large Database Endowment, 1(2):1265=961276, 2008.
4. S. Dar, M. J. Franklin, B. =DE=F3r J=F3nsson, D. Srivastava, M. Tan: Semantic Data Caching and Replacement. In Proceedings of the international conference on Very Large Data Bases, pages 330=96341, Bombay, India 1996.
5. C. Olston, B. Reed, U. Srivastava, R. Kumar, and A. Tomkins. Pig latin: a not-, so-foreign language for data processing. In Proceedings of the ACM SIGMOD, International Conference on Management of Data, pages 1099=961110, Vancouver, Canada, 2008.
6. Thusoo, J. S. Sarma, N. Jain, Z. Shao, P. Chakka, S. Anthony, H. Liu, P. Wyck-, off, and R. Murthy. Hive - a petabyte scale data warehouse using hadoop. In, Proceedings of the International Conference on Data Engineering, pages 996=961005, Long Beach, USA, 2010.
7. A. Vancea, L. d'Orazio, B. Stiller. A Scalable Cooperative Semantic Caching (CoopSC) Approach to Improve Range Queries. In Proceedings of the International Conference on Collaborative Computing, Networking, Applications and Worksharing, pages 1-11, Orlando, USA, 2011.
URL sujet détaillé : http://www.isima.fr/~dorazio/recherche/offres/m_cloud_caching.pdf
Remarques : Co-encadrement
- Pr. Dominique Laurent, ETIS, Université de Cergy Pontoise, Cergy Pontoise, France (dominique.laurent-=AD‐cergy.fr)
- Pr. Nicolas Spyratos, LRI, Université Paris Sud, Orsay, France (spyratos.fr)
Rémunération
Oui
Possibilité de thèse
Oui
|
|
|
|
|
|
SM207-37 Query rewriting in the cloud
|
|
|
Description
|
|
Context
In recent years, cloud computing has attracted increasing attention, especially under the leadership of suppliers such as Google, Microsoft, Amazon, Yahoo! or Facebook. Cloud computing aims at dealing with the growing needs in terms of computing and storage while being easily accessible. Particularly, clouds offer interesting perspectives for data analysis. Unfortunately, the performance of clouds are usually based on scalability relying on more computing nodes or more powerful ones, making the bill to pay higher for users and the use of resources far from optimal.
Performance optimization in databases has been studied for decades of years. The use of methods such as indexing, materialized views or caches within the cloud would improve overall performance by optimizing resource utilization. In particular, materialized views and semantic caches can rewrite posed queries in order to reuse the results of previous ones. However, these solutions are based on languages (SQL, XPath, etc.) or well-known data models (relational, semi-structured, etc.). As a consequence, they are not suited for languages available in the cloud.
Objectives
The first objective of this work is to study in detail the evaluation of query analysis, including OLAP queries that use GROUP BY clauses and aggregate calculations by considering the different query languages data available in the cloud: Pig Latin, HiveQL, SCOPE or Jaql. Existing solutions must be extended to take into account the specificities these languages.
It will then be important to propose rewriting rules for analysis queries for them to respect the elasticity property of the cloud. In addition, i twill be mandatory to consider specific operators that some languages include.
The model will then be developed and validated using infrastructures such as the cluster of the Université Blaise Pascal, Amazon EC2 or Grid5000.
Plan
The different milstones are:
1. Study of the evaluation of analytical queries with the data models and the languages proposed in the cloud,
2. Proposal of a rewriting model for analytical queries to be applied to semantic caching and materizalized views in the cloud relying on our previous work [5] [8]
3. Validation of the model using private infrastructure (Amazon, etc.).
References
1. M. Armbrust, A. Fox, R. Griffith, A. D. Joseph, R. H. Katz, A. Konwinski, G. Lee, D. A. Patterson, A. Rabkin, I. Stoica, and M. Zaharia. A view of cloud computing., Communications of the ACM, 53(4):50=9658, 2010.
2. K. S. Beyer, V. Ercegovac, R. Gemulla, A. Balmin, M. Y. Eltabakh, C.-C. Kanne, F. =D6zcan, E. J. Shekita: Jaql: A Scripting Language for Large Scale Semistructured Data Analysis. PVLDB 4(11): 1272-1283, 2011.
3. R. Chaiken, B. Jenkins, P.-=B0A. Larson, B. Ramsey, D. Shakib, S. Weaver, and, J. Zhou. Scope: easy and efficient parallel processing of massive data sets. Pro-, ceedings of the Very Large Database Endowment, 1(2):1265=961276, 2008.
4. S. Dar, M. J. Franklin, B. =DE=F3r J=F3nsson, D. Srivastava, M. Tan: Semantic Data Caching and Replacement. In Proceedings of the international conference on Very Large Data Bases, pages 330=96341, Bombay, India 1996.
5. D. Laurent, N. Spyratos. Rewriting Aggregate Queries using Functional Dependencies. In Proceedings of the International ACM Conference on Management of Emergent Digital EcoSystems 2011, San Francisco, USA, 2011.
6. C. Olston, B. Reed, U. Srivastava, R. Kumar, and A. Tomkins. Pig latin: a not-, so-foreign language for data processing. In Proceedings of the ACM SIGMOD, International Conference on Management of Data, pages 1099=961110, Vancouver, Canada, 2008.
7. Thusoo, J. S. Sarma, N. Jain, Z. Shao, P. Chakka, S. Anthony, H. Liu, P. Wyck-, off, and R. Murthy. Hive - a petabyte scale data warehouse using hadoop. In, Proceedings of the International Conference on Data Engineering, pages 996=961005, Long Beach, USA, 2010.
URL sujet détaillé : http://www.isima.fr/~dorazio/recherche/offres/m_cloud_rewriting.pdf
Remarques : Co-encadrement
- Pr. Dominique Laurent, ETIS, Université de Cergy Pontoise, Cergy Pontoise, France (dominique.laurent-=AD‐cergy.fr)
- Pr. Nicolas Spyratos, LRI, Université Paris Sud, Orsay, France (spyratos.fr)
Rémunération
Oui
Possibilité de thèse
Oui
|
|
|
|
|
|
SM207-38 Adaptiveness in Self-Stabilization
|
|
|
Description
|
|
The Distributed Programming Laboratory of EPFL proposes master and phd projects on the theory of distributed systems. These encompass multiprocessor as well as cluster and Internet environments. In short, the goal of the projects is to understand the power and limitations of distributed algorithms.
More specifically, one of the project we are working on is that of devising adaptive algorithms that have different complexities depending on the adversary at hand. The definition of adaptive algorithms is twofold. First, such algorithms have to be correct even if the algorithm runs under bad conditions (asynchronism, faults, contention...). Second, we require the algorithm to be efficient on the most probable executions (e.g. synchronous ones). In this way, we can guarantee safety of the system in any case but we provide an efficient algorithm from a practical point of view. In this project, we are seeking such adaptive algorithms in the context of self-stabilization where the goal is to tolerate transient faults (i.e., of finite duration) by guaranteeing that the system recovers from itself a correct behavior in a finite time after the end of transient faults. The goal of the project is to explore the feasibility of adaptiveness in the context of self-stabilization by studying classical problems of distributed computing (e.g. mutual exclusion, clock synchronization, maximal matching construction...).
The student will need to get familiar with the areas of distributed computing, fault-tolerance (ideally including self-stabilizing approaches), and algorithmic complexity; come up with ideas to prove impossibilities or devise algorithms and collaborate in the writing of a research paper, which would correspond to the master thesis.
URL sujet détaillé : http://lpd.epfl.ch/swdubois/pdf/DuboisGuerraouiEPFL.pdf
Remarques : Co-encadré par Swan Dubois, LPD, EPFL
contact : swan.dubois.ch
|
|
|
|
|
|
SM207-39 Géométrie aléatoire et mobilité dans les réseaux sans fil
|
|
|
Description
|
|
La géométrie stochastique est un outil mathématique probabiliste qui consiste en l'étude d'objets aléatoires distribués dans des espaces de dimension supérieures à 1. Ce sujet de stage porte sur l'étude de modèles de géométrie aléatoire pour l'étude des réseaux dynamiques. Les réseaux visés ici sont les réseaux sans fil.
Il existe de nombreux modèles de mobilité qui permettent de simuler les trajectoires des nóuds dans un réseau sans fil. Ces modèles de mobilité sont, dans la majorité des cas, utilisés lors de simulations pour estimer les performances des réseaux sans fil. Ils présentent l'inconvénient d'être complexe, et de prendre un nombre de paramètres important en entrée. Ceci rend les résultats observés difficilement généralisables. Le but de ce stage est de montrer que tous ces modèles peuvent être regroupés en un petit nombre de classes, ces classes présentant les mêmes propriétés. Les propriétés considérées ici sont celles du graphe de communication qui représente les liens sans fil existants entre les nóuds. Du point de vue du réseau, les propriétés importantes de ces graphes sont les temps de vie des liens (les temps de contacts), les fréquences des changements de voisinage, le degré, etc.
Le but de ce stage consiste en la proposition simple de modèle stochastique capturant les propriétés des modèles de mobilité. La première partie de ce stage portera sur des modèles de mobilité où l'essentiel des trajectoires des nóuds sont rectilignes (Random WayPoint model, Levy-Walk, etc.). Ces modèles seront rapprochés par des modèles de lignes issus de la géométrie stochastique.
URL sujet détaillé : http://www.anthonybusson.fr/sujet2012.pdf
Remarques :
|
|
|
|
|
|
SM207-40 Théorie des jeux appliquée à l'éco-efficience industrielle
|
|
|
Admin
|
|
| Encadrant : Denis GIEN |
| Labo/Organisme : LIMOS (Laboratoire d'Informatique de Modélisation et d'Optimisation des Systèmes) UMR 6158 |
| URL : http://limos.isima.fr/ |
| Ville : Clermont-Ferrand (Aubière) |
|
|
|
|
Description
|
|
L'éco-efficience industrielle vise à réduire les impacts environnementaux tout en améliorant la productivité. L'environnement économique et législatif introduit un fort couplage entre les actions des entreprises. La taxe carbone européenne, dont la troisième phase de mise en óuvre débute en 2013, est un exemple typique. Les efforts des entreprises vertueuses n'ont pas été récompensés à la hauteur des leurs attentes en raison de l'effondrement des cours du marché du CO2.
Le travail de recherche proposé est la modélisation de ce problème à l'aide de la théorie des jeux qui semble tout à fait pertinente dans ce contexte. Un modèle aussi complet que possible sera d'abord construit, pour un seul impact environnemental, en s'appuyant sur les informations disponibles. Le cas des émissions de CO2 est très intéressant dans la mesure où une évolution progressive de la législation est prévue sur la période 2013-2020. L'incidence de la croissance économique ou de mesures locales (nationales) pourra également être envisagée.
Le modèle sera ensuite simplifié pour permettre la réalisation d'une simulation, limitée à quelques entreprises, dans un contexte évolutif. Différentes stratégies et équilibres seront testés afin d'évaluer le potentiel de la théorie des jeux pour répondre à la problématique.
Références :
Bruce Mizrach, Integration of the global carbon markets, Energy Economics, Volume 34, Issue 1, January 2012, Pages 335-349.
Rui Zhao, Gareth Neighbour, Jiaojie Han, Michael McGuire, Pauline Deutz, Using game theory to describe strategy selection for environmental risk and carbon emissions reduction in the green supply chain, Journal of Loss Prevention in the Process Industries, Volume 25, Issue 6, November 2012, Pages 927-936.
URL sujet détaillé :
:
Remarques : Contexte : Le travail sera conduit au sein de l'équipe du LIMOS, travaillant sur la thématique du management environnemental, qui apportera son soutien pour la recherche d'informations relatives au domaine. La tâche demandée se limitera à la formalisation mathématique du problème et à la recherche d'équilibres. Cette recherche pourrait être poursuivie en doctorat avec pour objectif la proposition d'un système d'aide à la décision.
Localisation : L'équipe est hébergée à l'IFMA (Institut Français de Mécanique Avancée =96 Ecole associée à l'Institut Mines-Télécom).
Renseignements : Denis GIEN (PRU IFMA) =96 denis.gien.fr
|
|
|
|
|
|
SM207-41 Towards self-growing adaptable distributed applications
|
|
|
Description
|
|
General Topic:
=============This research project aims to address the following important question: how can software systems ensure their functional and quality goals, while having to frequently adapt their implementation and configuration in response to changes in their execution environment, internal faults or updates?
The self-growing software project =96 also called Cube (http://cube.imag.fr) - aims to address these antagonistic challenges. It proposes to allow software systems to self-assemble their internal compositions, at runtime, so as to make sure that their core functionalities and properties are being provided. Two main approaches are possible to achieve this objective - they both rely on software agents to self-assemble and adapt the targeted software system.
In one approach, an architectural template defines the targeted system that the agents must build and adapt; agent collaborations are constrained to those that produce applications that conform to the template.
In the other approach, agents manage to reach the same objective by repeatedly applying a set of carefully-designed rules; the properties of targeted applications are implicit in the rules.
Internship Objective:
====================This internship will explore the possibility of mixing the two aforementioned approaches in order to capitalise on their combined advantages. It will commence with the study of possible approaches and the analysis of their respective advantages, disadvantages and fields of applicability. This study will provide a solid base for the design and development of a mixed solution for self-growing software.
The targeted application consists of a self-growing monitoring infrastructure for adaptive distributed applications. Here, the distributed application can be self-grown based on the architecture-based approach. In parallel, a rule-based approach - to be developed - can be executed to create and adapt a monitoring infrastructure that follows the structure of the distributed application. Additionally, the monitoring infrastructure will self-adapt depending on the perceived state of the monitored application. In case of symptom detection, it will attempt to provide more detailed monitoring data by setting in place more monitoring elements. In normal conditions, it will attempt to minimise monitoring intrusions so as to avoid overheads.
URL sujet détaillé : http://infres.enst.fr/~diacones/stages/2013/internshipSubject_TPT2013.pdf
Remarques : Co-encadrement:
Prof. Isabelle Demeure et Dr. Hoa Dung Ha Duong
Possibilité de rémunération:
Oui (selon la grille de l'école)
|
|
|
|
|
|
SM207-42 Un radar pour l'internet
|
|
|
Description
|
|
Des millions de machines
échangent quotidiennement de l'information
via l'Internet. La surveillance du réseau (détection de pannes, d'attaques, d'anomalies logicielles, de zones saturées, ...)
est dans cette optique une problématique de première importance.
Il existe plusieurs approches pour atteindre ce but, mais le domaine
en est encore à ses balbutiements. L'approche graphes, qui s'intéresse aux variations de la structure du réseau plutôt qu'au trafic le traversant, semble prometteuse et n'a été
que très peu explorée pour l'instant. C'est dans ce contexte que
se situe ce stage.
Lorsqu'on est sur une machine de l'Internet (une source), il est possible
à l'aide de l'outil traceroute de connaître
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 mesurer
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 permanente qui va nous permettre de construire un
radar pour l'Internet.
Le stage proposé comporte plusieurs aspects (suivant les compétences spécifiques du stagiaire et ses centres d'intérêt,
l'accent pourra être mis sur l'un ou l'autre de ces aspects) :
- mise au point d'un outil de mesure périodique et de visualisation du voisinage d'une source,
- mise au point d'outils statistiques pour l'analyse de ces voisinages
et de leur dynamique,
- observation raisonnée de la vision obtenue et interprétation des phénomènes rencontrés,
- simulation et analyse formelle de la mesure et de la dynamique sur des modèles afin
d'évaluer la pertinence de l'information collectée.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2010/11/radar1.pdf
Remarques :
|
|
|
|
|
|
SM207-43 Modélisation des graphes de terrain
|
|
|
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 construits 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 hypertextes 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 lors, de nombreux travaux ont été menés visant à capturer ces propriétés dans des modèles, nécessaires tant pour effectuer
des simulations que pour étudier formellement ces objets, et bien sûr pour en comprendre la nature.
Les graphes aléatoires classiques capturent la densité faible (qui est en fait un paramètre du modèle) et la distance moyenne faible.
Par contre, ils ont une distribution des degrés homogène et une
densité locale faible.
Nous sommes également en mesure de générer un graphe aléatoire à
distribution de degrés donnée. On capture ainsi toutes les propriétés
citées ci-dessus sauf la densité locale forte.
Malgré de nombreuses tentatives, générer des graphes ayant
également une densité locale forte tout en gardant leur caractère reste un problème ouvert. Les attentes sont pourtant
extrêmement fortes.
Nous proposons d'attaquer ce problème sous deux angles nouveaux.
Dans la première approche, il s'agit de transformer la contrainte sur la densité locale forte en une contrainte sur les degrés.
L'autre approche repose sur la théorie des processus de branchements, qui
ont prouvé leur efficacité dans le contexte des graphes aléatoires mais
n'arrivent pas à capturer la densité locale.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2010/11/modelisation1.pdf
Remarques :
|
|
|
|
|
|
SM207-44 Dynamiques de graphes
|
|
|
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), le graphe 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,
est encore aujourd'hui largement à défricher.
Nous commençons aujourd'hui à disposer d'ensembles significatifs
de données sur des dynamiques de graphes. De plus, de premiers travaux,
bien qu'embryonnaires, montrent qu'il est effectivement pertinent de
proposer des méthodes générales pour l'analyse de telles dynamiques,
notamment (mais pas uniquement) avec des approches issues du traitement
du signal et de la théorie de l'information.
L'objectif de ce stage est de pousser plus avant les premiers
travaux effectués sur les dynamiques de graphes, en se concentrant
sur quelques cas particuliers (échanges pair-à-pair, topologie
de l'internet, ...). Il s'agit, par des
études de cas rigoureuses, d'identifier des paramètres pertinents
pour l'analyse des dynamiques de graphes. On s'intéressera également
aux applications de ces analyses.
URL sujet détaillé : http://www.complexnetworks.fr/wp-content/uploads/2010/11/dynamique1.pdf
Remarques :
|
|
|
|
|
|
SM207-45 The expressive power of equality constraint languages
|
|
|
Description
|
|
In this project we would like to obtain a classification of those structures that are preserved by all permutations and that additionally have a constant endomorphism. A basic open question is: are there countably or uncountably many such structures, up to primitive positive interdefinability? This problem is motivated
by questions concerning the computational complexity of constraint satisfaction problems.
URL sujet détaillé : http://www.lix.polytechnique.fr/~bodirsky/teaching/ecsp.pdf
Remarques : Co-encadrement avec Michael Pinsker
Gratification prevue
|
|
|
|
|
|
SM207-46 Mixed Nash equilibria in multiplayer concurrent games
|
|
|
Description
|
|
Games (and especially games played on graphs) have been intensively used in computer science as a powerful way of modelling interactions between several computerised systems [6, 4]. Until recently, more focus had been put on the study of purely antagonistic games (a.k.a. zero-sum games), useful for modelling systems evolving in a (hostile) environment.
Over the last ten years, non-zero-sum games have come into the picture : they are convenient for modelling complex infrastructures where each individual system tries to fulfill its objectives, while still being subject to uncontrollable actions of the surrounding systems. As an example, consider a wireless network in which several devices try to send data : each device can modulate its transmit power, in order to maximise its bandwidth and reduce energy consumption as much as possible. In that setting, focusing only on optimal strategies for one single agent may be too narrow, and several other solution concepts have been defined and studied in the literature, of which Nash equilibrium [5] is the most prominent. A Nash equilibrium is a strategy profile where no player can improve her payoff by unilaterally changing her strategy, resulting in a configuration of the network that is satisfactory to everyone. Notice that Nash equilibria need not exist or be unique, and are not necessarily optimal : Nash equilibria where all players lose may coexist with more interesting Nash equilibria.
Recently we have developed a complete framework that allows to compute pure (that is, deterministic) Nash equilibria in finite concurrent games with various types of objectives [1, 2, 3]. Pure Nash equilibria are however restricted joint behaviours of multiagent systems. The aim of this internship is to study mixed Nash equilibria in concurrent games, that is, equilibria that may require probabilistic choices. Techniques developed for pure Nash equilibria will need to be completely revised in order to take into account probabilities.
This internship will be part of ERC project EQualIS (http://www.lsv.ens-cachan. fr/~bouyer/equalis/), and can be extended into PhD studies (several PhD grants are available).
URL sujet détaillé : http://www.lsv.ens-cachan.fr/~bouyer/files/sujet-nash-proba.pdf
Remarques : Co-encadrant : Nicolas Markey (markey.ens-cachan.fr)
Possibilité de rémunération (projet ERC EQualIS).
Financement de thèse assuré (si le stage se passe bien).
|
|
|
|
|
|
SM207-47 Nash equilibria in multiplayer infinite-state games
|
|
|
Description
|
|
Games (and especially games played on graphs) have been intensively used in computer science as a powerful way of modelling interactions between several com- puterised systems [6, 4]. Until recently, more focus had been put on the study of purely antagonistic games (a.k.a. zero-sum games), useful for modelling systems evolving in a (hostile) environment.
Over the last ten years, non-zero-sum games have come into the picture : they are convenient for modelling complex infrastructures where each individual system tries to fulfill its objectives, while still being subject to uncontrollable actions of the surrounding systems. As an example, consider a wireless network in which several devices try to send data : each device can modulate its transmit power, in order to maximise its bandwidth and reduce energy consumption as much as possible. In that setting, focusing only on optimal strategies for one single agent may be too narrow, and several other solution concepts have been defined and studied in the literature, of which Nash equilibrium [5] is the most prominent. A Nash equilibrium is a strategy profile where no player can improve her payoff by unilaterally changing her strategy, resulting in a configuration of the network that is satisfactory to everyone. Notice that Nash equilibria need not exist or be unique, and are not necessarily optimal : Nash equilibria where all players lose may coexist with more interesting Nash equilibria.
Recently we have developed a complete framework that allows to compute pure Nash equilibria in finite concurrent games with various types of objectives [1, 2, 3]. The aim of this internship is to pursue our study of Nash equilibria in multiagent systems, by extending the above approach to infinite-state games. We propose to first study push- down and one-counter games. Then we target more quantitative models like weighted games or timed games.
This internship will be part of ERC project EQualIS (http://www.lsv.ens-cachan. fr/~bouyer/equalis/), and can be extended into PhD studies (several PhD grants are available).
URL sujet détaillé : http://www.lsv.ens-cachan.fr/~bouyer/files/sujet-nash.pdf
Remarques : Co-encadrant : Nicolas Markey (markey.ens-cachan.fr)
Possibilité de rémunération (projet ERC EQualIS).
Financement de thèse assuré (si le stage se passe bien).
|
|
|
|
|
|
SM207-48 Gathering Entropy from Solid State Drives
|
|
|
Description
|
|
Context
Random Number Generators constitute a fundamental building block of computer security. They produce unguessable "secrets" which are necessary to guarantee message integrity, communica- tion confidentiality, and other security properties.
Basically, the architecture of a generator can be divided in two distincts parts. Actual numbers are produced by a so-called Cryptogaphically Secure Pseudo-Random Number Generator, i.e. a numerical algorithm which, depsite being completely deterministic, guarantees good statistical properties about its output. But in order to achieve actual randomness, the internal state of this algorithm has to be randomly "refreshed" from time to time. For this purpose, a second component of the generator is in charge of harvesting so-called "entropy sources", i.e. observing unpredictable events in the system, like the variability of hard disk seek times.
While the algorithmic aspect of random number generation has been studied extensively, the entropy generation process itself is not well understood. This is the subject we are interested in. Hard disk drives are traditionally considered the major source of entropy in a computer system, and most previous works were based on the assumption of a mechanical disk. However, solid-state drives are now becoming mainstream, and they have the reputation of beeing poor entropy providers due to their greater predictability. This challenges the design of existing random number generators.
Goals
The student will have to characterize the timing behaviour of solid-state drives by doing both a litterature study and empirical experiments on actual hardware. Then, the goal of this work is to identify which mechanisms in solid-state drives can provide entropy. Following these results, we plan to modify the Linux Random Number Generator to improve its robustness.
URL sujet détaillé : http://perso.citi.insa-lyon.fr/gsalagnac/files/stage-entropie.pdf
Remarques :
|
|
|
|
|
|
SM207-49 Agrégation de séries temporelles de graphes
|
|
|
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é?
URL sujet détaillé :
:
Remarques : Stage co-encadré par Eric Fleury (LIP, ENS de Lyon)
|
|
|
|
|
|
SM207-50 Criticalité quantique dans différents matériaux
|
|
|
Description
|
|
Ce stage est consacré à l'étude de la criticalité quantique dans différents types de matériaux.
Nous regarderons en détails les effets des fluctuations quantiques
dans le cas du Point Critique Quantique (PCQ) de Peierls
dans les supraconducteurs organiques, étudiés depuis de nombreuses années par le groupe de Denis Jérome à Orsay. Nous regarderons aussi le cas du PCQ anti-ferromagnétique à deux
dimensions d'espace, considéré comme étant un ingrédient important de la théorie des supraconducteurs à haute température critique, pour lequel nous avons récemment obtenu un résultat remarquable avec l'émergence d'un pseudo-gap à proximité du PCQ. L'étude de ces nouveaux états de la matière
en est encore à ses débuts et beaucoup de travail reste à faire, comme de déterminer quelle situation expérimentale sera le révélateur de ces états quantiques. Dans ce travail de stage, nous travaillerons sur trois tableaux : analytique ( modèle sigma non linéraire, bosons esclaves, RG, théorie à N corps), couplage aux expériences ( beaucoup d'expérimentateurs sont dans la région, que ce soit dans le cas des supraconducteurs à haute Tc que des organiques) ainsi qu'un peu de travail numérique.
Ce stage pourra déboucher sur une thèse.
URL sujet détaillé :
:
Remarques : Possibilité de déboucher sur une thèse. Discussions avec les expérimentateurs du plateau. Petite rémunération du labo.
|
|
|
|
|
|
SM207-51 Contribution à l'étude de la modélisation déclarative de surfaces à pôles
|
|
|
Description
|
|
Alors que les surfaces à pôles correspondent aujourd'hui au modèle mathématique très utilisé pour la Conception Assistée par Ordinateur (CAO) et ont depuis longtemps prouvé leur efficacité (il suffit de regarder les objets qui nous entourent au quotidien), il y a encore trop peu d'outils de haut niveau permettant d'assister le concepteur dans sa démarche créative. La modélisation déclarative de surfaces se propose d'offrir de tels outils en passant par la description intuitive des formes que l'utilisateur souhaite obtenir. Des travaux ont déjà été entrepris dans ce domaine, mais il reste encore de nombreuses pistes à explorer et verrous scientifiques à lever afin de permettre à un néophyte de créer des surfaces à l'aide de règles de description de haut niveau liées à la sémantique métier de l'application visée.
Le projet de recherche a pour objet de contribuer à la modélisation de surfaces à l'aide d'une approche déclarative. La priorité sera donnée aux surfaces à pôles (Bézier, B-splines voire NURBS), mais une réflexion sur les surfaces de subdivision (la base des films d'animation) est envisageable.
Le domaine est particulièrement vaste et des choix devront être faits parmi un ensemble de verrous scientifiques :
- techniques de description
- transcription des propriétés en des contraintes exprimables sur un ordinateur
- résolution de contraintes géométriques.
La première phase du projet consiste à comprendre la problématique et l'existant. Ensuite, il s'agira de se fixer des objectifs raisonnables afin de les conduire à terme.
La résolution de contraintes géométriques fera nécessairement partie du travail à réaliser. Il faut être conscient que cet aspect est un thème de recherche à lui seul, et qu'il faudra donc le limiter en tenant compte en particulier du contexte lié au modèle mathématique manipulé. Une attention sera porté sur le fait que cette approche peut conduire à des problèmes globalement sous-contraints, sur-constraints et même sous ou sur-contraints localement.
C'est évidemment un travail qui peut se poursuivre au delà de ce stage de master. C'est un sujet difficile mais qui intéresse de nombreuses équipes en France. Des collaborations avec d'autres équipes de recherche seront donc naturelles. Il y a évidemment des débouchés industriels à termes, mais la recherche doit encore progresser pour que les résultats intéressent réellement les industriels.
URL sujet détaillé : il est préférable que le candidat intéressé me contacte pour discuter que de faire un long texte sur ce projet
:
Remarques :
|
|
|
|
|
|
SM207-52 Génération de code pour l'évaluation des fonctions élémentaires
|
|
|
Description
|
|
La bibliothèque mathématique (libm) est un composant du système d'exploitation qui offre les fonctions élémentaires (exponentielle, logarithme, fonctions trigonométriques et leurs inverses, fonctions hyperboliques, ...) et certaines fonctions spéciales courantes (erf, gamma, ...). La performance est critique, puisque de nombreuses applications de calcul intensif passent une fraction importante de leur temps à évaluer de telles fonctions. Chaque évolution du processeur demande à réévaluer la pertinence des choix algorithmiques faits: des équipes d'ingénieurs, chez les principaux constructeurs de processeurs, travaillent à réimplémenter la libm sur chaque nouveau processeur. De plus, il y a même depuis peu plusieurs versions de chaque fonction: différents contextes ont besoin de différentes spécifications, que ce soit en terme de performance (minimiser la latence, ou maximiser le débit du calcul), ou en terme de précision (favoriser la précision et la reproducibilité des calculs, ou favoriser la performance au détriment de la précision).
Mais face à cette complexité, les fonctions elles-mêmes, en tant qu'objets mathématiques, n'évoluent pas: leur implantation est basée sur une collection limitée de recettes bien connues. Le développement d'un libm est donc actuellement un art qui consiste à assembler au mieux ces recettes, pour maximiser la performance sous une contrainte de précision. L'objet de ce stage est de formaliser cet art, dans le but d'automatiser l'expertise mise en jeu.
Concrètement, une fonction élémentaire est facile à approcher par un polynôme sur un petit intervalle. L'état de l'art pour l'approximation polynomiale est l'outil Sollya, développé par l'équipe AriC. Nous avons aussi développé l'outil Gappa, un assistant de preuve qui permet de borner les erreurs d'arrondi dans les codes flottants typiques des libm. Il reste à formaliser celles des recettes évoquées plus haut qui servent à se ramener dans la situation où l'approximation polynômiale est pertinente. Ces recettes devront être exprimées comme une réécriture d'une expression mathématique en une autre, avec éventuellement un calcul d'erreur (d'approximation et/ou d'arrondi) associé. La réécriture, comme le calcul d'erreur, devront être programmés. L'idée est de réécrire graduellement l'arrondi d'une fonction mathématique vers un flottant en un code qui l'implémente avec une précision garantie. Les études de cas considérées dans ce stage seront les fonctions trigonométriques et leurs inverses.
L'intérêt de ce stage est donc de couvrir un spectre qui va des mathématiques (analyse et calcul d'erreur fin) jusqu'à l'implémentation de bas niveau (en langage C).
URL sujet détaillé :
:
Remarques : Rémunération possible.
|
|
|
|
|
|
SM207-53 Dynamique des groupes
|
|
|
Description
|
|
La compréhension des mécanismes comportementaux et des interactions qui gouvernent la dynamique des groupes constitue une question fondamentale en sciences du comportement, en sciences sociales et en informatique répartie. De nouvelles techniques de capture et de traitement en temps réel des déplacements et des interactions d'un grand nombre d'individus comme la plateforme Souk (Spatially Observing hUman Kinetics) développée au LAAS-CNRS permettent aujourd'hui une approche quantitative de ces phénomènes dans leurs dimensions spatiales et sociales.
L'objectif de ce stage est d'exploiter conjointement les dynamismes spatiaux et sociaux afin de comprendre leurs relations. Autrement dit, il s'agit d'utiliser l'une des mobilités pour comprendre l'autre.
A partir des données recueillies par la plateforme Souk au cours d'une manifestation ayant rassemblé une centaine de personnes, on analysera plus spécifiquement la dynamique de formation/déformation des groupes, les déplacements des participants et les graphes d'interaction entre ces derniers.
A titre d'exemple, nous chercherons ainsi à modéliser certains comportement afin de répondre a des questions du type : " les personnes influentes se déplacent-elles différemment des personnes ordinaires ? ", " Comment prévoir la dissolution d'un groupe de discussion ? Sa stabilité dans le temps ? L'évolution de sa taille? ", " Peut-on prédire les rencontres ? ". L'angle de cette analyse sera celui du développement de modèles de dynamique et d'interaction, ainsi que de primitives logicielles robustes à ces dynamiques.
Ce stage se situe à mi-chemin entre l'analyse exploratoire de données, la modélisation, l'analyse de réseaux sociaux, et l'algorithmique distribuée. Nous cherchons des candidats motivés et autonomes possédant de solides bases en statistiques/estimation/théorie des graphes/algorithmique.
URL sujet détaillé :
:
Remarques : Co-encadrement avec :
Gilles Trédan (CR CNRS - LAAS)
Guy Théraulaz (DR CNRS - Laboratoire de Recherche sur la Cognition Animale)
Possibilité de rémunération.
Possibilité de poursuivre en thèse.
|
|
|
|
|
|
SM207-54 Reasoning on Graph Transformations
|
|
|
Description
|
|
There is a growing practical interest in using graph rewriting
techniques in several domains such as software architecture,
programming theory, model-driven engineering, semantics of visual
modeling frameworks (e.g. UML), but also bio-informatics, system
biology, DNA computing, Artificial Intelligence and quantum
computing to quote a few. Despite the progress made so far in graph
transformation theory [1,2,3], there are still many obstacles that
prevent wider use of graph transformations.
Nowadays there are only first steps exploring the question of the
correctness of graph transformations (see e.g. [4,5,6]). Logic-based
methods of reasoning about graph transformations are far from being
well established, but are recently gaining momentum. In the past few
years, there has been a flurry of interest in specialized logics such
as separation logic, variants of first order logic, monadic second
order logic, dynamic (modal) logics etc. The aim of this internship
is to device new proof techniques dedicated to reason on graph
transformations. Successful candidate may pursue her/his investigation
on this topic when entering a PhD program. This internship is part of
a national basic research project funded by the ANR (Agence Nationale
de la Recherche). More details are available from the supervisor
(echahed.fr).
[1]H.Ehrig, G.Engels, H.-J. Kreowski, and G.Rozenberg, editors. Handbook of Graph Grammars and Computing by Graph Transformations, Volume 2: Applications, Languages and Tools. World Scientific, 1999.
[2]H.Ehrig, H.-J. Kreowski, U.Montanari, and G.Rozenberg, editors.Handbook of Graph Grammars and Computing by Graph Transformations, Volume 3: Concurrency, Parallelism and Distribution. World Scientific, 1999.
[3]G.Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations. World Scientific, 1997.
[4]Ch. Blume, H.J.S. Bruggink, D. Engelke, B. K=F6nig: Efficient Symbolic Implementation of Graph Automata with Applications to Invariant Checking. In Procs. of the 6th International Conference on Graph Transformations (ICGT 2012): 264-278
[5]Ch. M. Poskitt: Verification of Graph Programs. In Procs. of the 6th International Conference on Graph Transformations (ICGT 2012): 420-422
[6]A. Vandin: Specification and Verification of Modal Properties for Structured Systems. In Procs. of the 6th International Conference on Graph Transformations (ICGT 2012): 423-425
URL sujet détaillé :
:
Remarques : possibilité de rémunération, possibilité de poursuivre en thèse (allocation, bourse)
|
|
|
|
|
|
SM207-55 Stochastic blockmodels for large-scale information networks
|
|
|
Description
|
|
Context:
Due to recent developments of the Web, huge amounts of structured data are becoming increasingly available, most notably in the form of information networks. Online exchange of information often tends to organize itself through some sort of network, where relevant examples include friendship networks (Facebook), customer-product networks (Amazon), co-authorship and citation networks (DBLP, Google Scholar). Massive application of statistical methods is a crucial element of Web technologies such as search engines, spam filters, or recommender systems. But although statistical machine learning has achieved a solid understanding of uncertain and noisy data whenever they can be formalized as fixed-length feature vectors, we are still far from reaching a general consensus on the correct way of modeling networks as statistical objects. As a consequence, a large variety of statistical models have been proposed recently, but none of them has been generally adopted as a standard reference.
Objectives:
This internship will focus on stochastic blockmodels (and possibly on other models from the same family), which are one of the main options developed in the literature on random networks. The goal is to achieve a firm understanding of the model strengths and weaknesses, both from the theoretical and the experimental point of view. The main theoretical problem to investigate concerns the treatment of variable correlations, along with the involved independence hypotheses. On the other hand, a crucial question that must be addressed experimentally concerns the performance of such models in real world applications such as link-prediction or graph generation. Background questions involved in the analysis relate to the inference algorithms supported by stochastic blockmodels, as well as to the computational complexity of model estimation, questions that can be approached both from a theoretical and an experimental point of view.
URL sujet détaillé :
:
Remarques : The project will be co-supervised by Marc Tommasi (http://researchers.lille.inria.fr/~tommasi/).
|
|
|
|
|
|
SM207-56 Expansions virgule flottante
|
|
|
Description
|
|
De nombreux problèmes numériques demandent parfois à faire appel à une plus grande précision que celle offerte par les formats virgule flottante usuels. Une solution est de faire appel à des bibliothèques multi-précision telles que mpfr (http://www.mpfr.org), mais c'est une solution assez lourde lorsqu'une précision de quelques centaines de bits suffit et qu'une grande performance est nécessaire. Dans ces cas-là, une meilleure solution peut être la manipulation "d'expansions virgule flottante". Une expansion virgule flottante est constituée de la somme non-évaluée de quelques nombres virgule flottante a_1, a_2, ..., a_k (en pratique k est tout petit, au plus 8), telle que a_1>> a_2>> a_3>> ... (en fait les contraintes sont plus fortes que cela et dépendent des auteurs).
Des algorithmes de manipulation d'expansions (addition, multiplication, division, etc.) ont été proposées par divers auteurs, comme Priest, Shewchuk, ou Bailey. Plusieurs de ces algorithmes ont été publiés sans preuve convaincante (voire sans preuve du tout dans le cas de certains algorithmes de Bailey). Le projet est de "nettoyer" ces connaissances, en donnant une présentation rigoureuse et des preuves solides, en choisissant les bons algorithmes et en en proposant des implantations efficaces de ces algorithmes.
De nombreux exemples de problèmes qui doivent utiliser / ont utilisé des
expansions à virgule flottante (double-double, quad double, sommes
compensées) sont liées au processus d'itération a longue terme (long
time iteration) de systèmes dynamiques chaotiques. Une plus grande
precision est nécessaire dans ce vaste domaine, allant de l'étude des
propriétés mathématiques de systèmes dynamiques classiques tels que
"l'attracteur de Henon", aux questions liées à la stabilité du système
planétaire, où les calculs d'orbites planétaires doivent être effectuées
sur des périodes cosmologiques - des milliards d'années (voir par exemple les travaux de Jacques Laskar).
Concernant les applications aux systemes dynamiques chaotiques, le
projet se fera en collaboration avec l'equipe CAPA
http://www2.math.uu.se/~warwick/CAPA/, de l'Université d'Uppsala, en Suède. Il peut se poursuivre par une thèse (c'est même une perspective souhaitée).
Le stage sera co-encadré par Mioara Joldes et Jean-Michel Muller. Il sera rémunéré.
Petite bibliographie:
J. R. Shewchuk. Adaptive precision floating-point arithmetic and fast robust geometric predicates. Discrete Computational Geometry, 18:305=96 363, 1997.
D. M. Priest. Algorithms for arbitrary precision floating point arith- metic. In P. Kornerup and D. W. Matula, editors, Proceedings of the 10th IEEE Symposium on Computer Arithmetic (Arith-10), pages 132=96144. IEEE Computer Society Press, Los Alamitos, CA, June 1991.
URL sujet détaillé :
:
Remarques : - le stage sera rémunéré
- il sera co-encadré par Mioara Joldes (actuellement à l'Université D'Uppsala, et qui va bientôt rejoindre le LAAS à Toulouse)
|
|
|
|
|
|
SM207-57 Reconstruction du répertoire VDJ par séquençage haut-débit
|
|
|
Description
|
|
== Thématiques : algorithmique du texte, bioinformatique
== Contexte
La leucémie aigue lymphoblastique (ALL, Acute Lymphoblastic Leukemia) est un cancer liquide touchant principalement les enfants. Le taux de survie des patients affectés par une ALL a nettement augmenté dans les dernières décades, grâce à des diagnostics plus précis et aussi une meilleure stratégie thérapeutique. Le diagnostic de ALL demande d'analyser les lymphoblastes et les lymphocytes, en dénombrant ces cellules selon leur réarrangement VDJ, réarrangement donnant des milliards de possibilités différentes à partir d'un répertoire de quelques gènes. Les patients sont suivis tout au long de leur traitement, des prélèvements sanguins sont effectués à intervalles réguliers afin d'identifier toute rechute. La méthode utilisée pour le suivi consiste à évaluer la concentration des lymphoblastes possédant le même réarrangement VDJ que lors du diagnostic.
Des études se sont intéressées à la diversité de ces réarrangements, telles que (Boyd, 2009), mais n'ont pas été vers une évaluation quantitative des " profils VDJ ". Une autre étude plus récente (Warren, 2011) a permis d'établir une première borne minimale du nombre de lymphoblastes différents. Cependant, en raison des techniques utilisées, cette étude ne permet pas réellement d'avoir une idée de la distribution des différents réarrangements au sein d'un échantillon et, a fortiori, de leur évolution chez un patient malade. De plus cette borne minimale est très loin des bornes théoriques (1 million contre plusieurs milliards).
== Problématique
Ce projet s'inscrit dans une collaboration entre l'équipe Bonsai du LIFL, la plateforme de séquençage de Lille 2 et de l'IRCL, et le laboratoire d'hématologie du CHRU de Lille. Notre nouvelle approche s'appuie sur les progrès colossaux réalisés dans le domaine du séquençage de l'ADN via les séquenceurs à haut débit, capable de séquencer des millions de séquences en quelques heures. Trois "runs" de test ont déjà été effectués en 2011 et 2012 pour séquencer les lymphocytes de patients suivis au CHRU.
Un prototype permettant l'analyse de la concentration des lymphoblastes en fonction de leur réarrangement VDJ a été développé au sein de l'équipe Bonsai. Le développement de ce prototype continuera en 2013. Les premiers résultats sont satisfaisants et permettent de retrouver, sur des donnés patient, des résultats précédemment validés par les cliniciens. Cette méthodologie permet de mieux comprendre la maladie résiduelle : comment émergent de nouveaux clones, comment évoluent-ils ?
== Travail à réaliser
Les études existantes, telles que (Boyd, 2009, Sci Transl Med) tout comme notre prototype, se basent toutes sur un " répertoire VDJ " humain connu. Si cela permet une assignation rapide, cetten méthode ne permet pas d'analyser les réarrangements VDJ lorsque le répertoire du patient diffère beaucoup du répertoire de référence. Le stage vise donc à proposer des algorithmes permettant une analyse à large échelle des réarrangements VDJ sans a priori, c'est à dire sans partir d'un répertoire VDJ de référence. Le but est double : améliorer les connaissances fondamentales sur la diversité de ces répertoires et ce des profils VDJ, et disposer de meilleurs outils pour le diagnostic et le suivi des leucémies.
Concrètement, le stage débutera par une étude bibliographique sur des techniques avancées d'algorithmique du texte (pattern matching, graines, indexation, filtrage) mais aussi sur le domaine biologique. Puis le stagiaire étudiera des algorithmes pour obtenir, à partir d'un ensemble de reads provenant de quelques individus, leurs " profils VDJ ", c'est-à-dire le répertoire des gènes VDJ qui ont été séquencés ainsi qu'une mesure de la présence des différents réarrangements VDJ au sein d'un échantillon. Nous souhaitons explorer des pistes prometteuses utilisant le dénombrement et classification de k-mers découpés sur les reads.
Les idées propososées durant le stage seront implémentées et expérimentées, sur des ensembles de reads simulés puis réels, issus de patients suivis au CHR de Lille.
== Poursuite en thèse
Être capable d'analyser systématiquement les profils VDJs permet d'envisager des études qui dépassent largement le cadre des leucémies : comment une réaction immunologique se traduit, quantitativement, sur le profil VDJ d'un individu ? Au sein d'une population, quelles sont les variations entre les profils VDJ de plusieurs individus ?
Répondre à ces questions demande d'avoir de puissants outils algorithmiques. Ce stage de M2 pourrait donc se poursuivre par une thèse sur la conception de structures de données adaptées au stockage et la comparaison de profils VDJ sur une population de plusieurs individus. Les structures d'indexation habituellement utilisées (arbres et tables de suffixes) ne sont en effet pas adaptées au stockage de telles informations.
== Compétences requises
Algorithmique du texte
Programmation en C/C++
Intérêt pour la biologie
== Bibliographie (envoyée sur demande)
K. J. L. Jackson and al., Benchmarking the performance of human antibody gene alignment utilities using a 454 sequence dataset, Bioinformatics, 26(24), 3129-3130
E. Market and F. N. Papavasiliou, V(D)J Recombination and the Evolution of the Adaptive Immune System, PLoS Biology 1(1):e16
S. D. Boyd and al., Measurement and clinical monitoring of human lymphocyte clonality by massively parallel VDJ pyrosequencing, Sci Transl Med. 2009 December 23; 1(12): 12ra23.
René L. Warren et al., Exhaustive T-cell repertoire sequencing of human peripheral blood samples reveals signatures of antigen selection and a directly measured repertoire size of at least 1 million clonotypes, Genome Research 21, 5, 790-797, 2011
URL sujet détaillé :
:
Remarques : Stage co-encadré par Mikaël Salson, LIFL
|
|
|
|
|
|
SM207-58 Interprétation fonctionnel des systèmes de réécriture de mots (non associatifs)
|
|
|
Description
|
|
Les systèmes de réécriture de termes sont habituellement présentés comme la donnée d'une relation binaire (le pré-ordre compatible avec les opérations engendré par des règles de réduction élémentaires). Cependant un point de vue fonctionnel est employé par George M. Bergman dans son article <>, Advances in Mathematics 29 (1978) 178-218 dans le cadre de la réécriture dans un anneau libre. Patrick Dehornoy et Vincent Van Oostrom exploitent également un point de vue similaire -- mais avec de subtiles différences -- dans <>, Mathematical Structures in Computer Science 18 (6) (2008) 1133-1167. L'objectif du stage est de comparer les deux approches fonctionnelles dans le cadre de la réécriture sur un magma libre puis traduire dans le cadre introduit par George M. Bergman certains des résultats obtenus par Patrick Dehornoy et Vincent Van Oostrom.
URL sujet détaillé : http://dl.dropbox.com/u/19919207/Rewriting_systems.pdf
Remarques : Le stage sera rémunéré.
|
|
|
|
|
|
SM207-59 Ordonnancement de threads sur processeurs multi-coeurs
|
|
|
Description
|
|
Avec l'introduction massive des processeurs multi-cóurs, le parallélisme entre dans une nouvelle ère technologique. Il devient un domaine plus large, plus accessible en coût, et s'ouvre à de nouvelles applications qui étaient jusqu'à présent concentrées sur les calculs scientifiques hautes performances. Nous constatons cependant que les temps d'exécutions des programmes parallèles sur processeurs multi-cóurs sont d'une très grande volatilité. De telles variations non négligeables des performances s'expliquent par plusieurs facteurs qui se combinent, tant à la fois au niveau logiciel (facteurs intrinsèques au code parallèle, facteurs intrinsèques à l'intergiciel et au système d'exploitation) et au niveau matériel (micro-architecture). Cette volatilité cause de sérieux problèmes de stabilité des performances, elle rend difficile une prédiction précise des performances des programmes. Également, elle complique les comparaisons entre plusieurs versions de la même application. Afin d'avoir une analyse pertinente des performances des programmes, cette thèse étudiera les facteurs influant la variabilité des performances des applications parallèles sur processeurs multi-cóurs et proposera des approches de les stabiliser.
>
URL sujet détaillé :
:
Remarques : Stage rémunéré (entre 500 et 1000 euros net selon profil).
Possibilité de poursuite en thèse.
|
|
|
|
|
|
SM207-60 Optimisation de chemin dans un graphe d'échafaudage et application au génome d'Ostreococcus Tauri
|
|
|
Description
|
|
Avertissement : Ce sujet est destiné à des étudiants compétents en théorie des graphes et en complexité, et ne nécessite aucun pré-requis bioinformatique autre qu'une curiosité pour le sujet.
Les données de séquençage de génomes se trouvent au départ sous la forme de très nombreux petits morceaux de séquence (quelques dizaines de paires de bases), appelés des reads. Ensuite, on assemble ces reads, de manière à tenir compte de leurs chevauchements, afin de déterminer des portions de génomes plus conséquentes, que l'on nomme contigs.
Objectif du stage :
Nous nous intéresserons au cours de ce stage à la troisième étape de la production d'un génome complet, à savoir comment ordonner les contigs et les placer sur les chromosomes de manière à obtenir une information complète et cohérente. Il s'agit de l'étape du scaffolding, ou échafaudage. L'idée générale est de partir de la donnée des contigs, et d'un ordre total supposé sur ceux-ci, et d'analyser a posteriori le mapping des reads sur les contigs.
Plus précisément, les reads vont par paires, qui correspondent aux extrêmités des petits morceaux séquencés. Ces paires de reads apportent de l'information significative. Par exemple si l'on considère deux contigs, ils peuvent contenir chacun l'extrêmité d'une paire, ce qui tendrait à signifier que l'on peut combler le "trou" entre ces deux contigs et les fusionner.
En considérant les contigs comme les sommets d'un graphe dont les arêtes représentent les liens déterminés par les extrêmités des paires de reads, le problème du scaffolding devient un problème de détermination d'un chemin hamiltonien avec de "bonnes" propriétés dans ce graphe, ce qui est évidemment très classiquement un problème de type voyageur de commerce (TSP).
Mais cette approche donne une réponse un peu trop simpliste au problème initial, car on ne tient pas compte des autres informations fournies par le mapping des reads sur les contigs. L'objectif du stage est d'intégrer ces différentes dimensions et d'étudier leur impact sur la formalisation du problème et sa résolution.
URL sujet détaillé : http://www.lirmm.fr/~chateau/sujet_scaffolding_optim.pdf
Remarques :
|
|
|
|
|
|
SM207-61 Etude d'un model neural pour comprendre mieux l'action de l'anesthesie
|
|
|
Description
|
|
L'importance de l'anesthesie dans la pratique hospitaliere n'est plus a demontrer. Il est moins connu que les
anesthesiques changent l'activite oscillatoire du cerveau. Par exemple, ce changement d'activite cerebrale
mesure par l'electroencephalogramme (EEG) en pratique hospitaliere indique la profondeur de l'anesthesie
du patient. Bien que la procedure experimentale de l'anesthesie soit bien etablie, on connait peu de choses
sur les effets du produit anesthesique sur le reseau neuronal.
Ce projet a pour but d'etudier en details les effets des anesthesiques sur des seules neurones, pour mieux
comprendre l'action neurale des anesthesiques, connus a partir d'experimentation telles que les modifications
d'EEG en pratique hospitaliere. L'etudiant commencera par une etude de la litterature sur les modeles neuronales
et les proprietes des recepteurs inhibiteurs synaptiques et extra-synaptiques, qui jouent un role majeur en anesthesie.
Apres il/elle va etudier analytiquement et numeriquent un model de neuron standard (Leaky Integrate-and-Fire)
sous l'effet de l'anesthesique propofol. Comme l'anesthesique modifie l'activite oscillatoire des populations des
neurones, le projet finira avec une etude numerique d'une population neurale.
En cas optimale, l'etudiant peut maitriser l'analyse mathematique des equations differentielles lineaires, a du
connaissance d'une langue programmation (C,C++ ou Python) ou logiciels equivalents (Matlab) et s'interesse
au neuroscience theorique.
URL sujet détaillé : http://www.loria.fr/~huttaxel/filez/Projet_Master2_engl.html
Remarques :
|
|
|
|
|
|
SM207-62 Complexité d'énumération
|
|
|
Description
|
|
En complexité on s'intéresse généralement au temps nécessaire pour décider si un problème a une solution et éventuellement la produire.
La complexité d'énumération étudie les algorithmes qui produisent toutes les solutions d'un problème. Dans ce contexte on étudie la dynamique de l'algorithme c'est-à-dire le délai entre la production de deux solutions.
Les problèmes d'énumération apparaissent naturellement
quand on s'intéresse à l'optimisation ou aux requêtes sur les bases de données. Il s'agit ici d'étudier leur complexité d'un point de vue théorique.
On obtient parfois des résultats étonnants, par exemple trouver un couplage parfait dans un graphe est facile, compter leur nombre est difficile
et tous les produire est facile. Énumérer les ensembles indépendants maximaux d'un graphe dans l'ordre lexicographique est facile mais c'est dur
dans l'ordre anti-lexicographique.
On voudrait séparer deux classes de complexité: le délai polynomial et le délai incrémental.
Dans le premier cas, le temps entre la production de deux solutions est polynomial en l'entrée tandis que dans le deuxième il est polynomial en le nombre de solution produites (et augmente donc au cours de l'algorithme).
Plusieurs voies existent pour attaquer ce problème.
La première est d'utiliser des hypothèses de complexité fortes comme
celle du temps exponentiel (SAT ne se résout pas en temps sous-exponentiel).
Une seconde qui sera exploré en priorité sera de comprendre
la génération de solutions par règle de clôture.
L'idée est qu'on part avec un ensemble de solution et qu'une règle simple permet de composer ces solutions pour en créer de nouvelles.
Quand on ne peut plus en créer, on les a toutes trouvées. Ce genre de procédure est naturellement à délai incrémental.
Pourtant une étude des règles les plus simples (compositions ensembliste comme l'union, l'intersection ...)
montre qu'on peut les produire en délai polynomial. Il s'agit d'entreprendre une étude systématique de ces règles de composition
pour les classifier selon qu'elles donnent des problèmes à délai polynomial ou incrémental.
Ce genre d'étude fera sans doute intervenir des idées venant des CSP comme les polymorphismes
ou les treillis de Gallois afin d'obtenir un théorème de dichotomie.
Plus de détails sur la complexité d'énumération peuvent être trouvés sur mon site web, notamment une introduction dans ma thèse.
URL sujet détaillé :
:
Remarques : Un co-encadrement et une éventuelle poursuite en thèse sont possibles. Ne pas hésiter à me contacter pour des questions.
|
|
|
|
|
|
SM207-63 Interaction between game theory and statistical learning
|
|
|
Description
|
|
Background:
In the last decades, the field of machine learning has had an enormous expansion, which resulted in very sophisticated algorithms able to learn, based on training data, how to perform tasks such as prediction or classification. These algorithms have been successfully used for quite some time in many applications such as recommendation, search engines or spam filters. For example, for spam filters, the algorithm uses a number of features to classify an email as spam or regular.
In more recent years, researchers have observed that it is possible (and relatively easy) for a smart attacker who knows what learning algorithm is used, to manipulate the training set in order to make the classification algorithm fail [1,2]. The learning algorithm can be adapted in consequence, but then the attacker would know the new algorithm, and so on. The interaction between the learning algorithm designer and the attacker can be analyzed using game theory. Such analyses appeared very recently in simplistic cases [3,4,5], but most of the topic remains open.
Objectives of the internship:
The goal of this internship is to analyze the interaction between a learning algorithm and an attacker, using the example of a spam filter. Starting from a standard spam filter (e.g., SpamBayes), the student will elaborate a game-theoretic model of the interaction between the two players. Then, he/she will search for methods to compute the Nash equilibria, and try to evaluate the loss of utility incurred by the spam filter due to the fact that the attacker is strategic. The student will start with a model in the static case (one-shot game). Later, the dynamic case where the attacker can induce inaccurate training for future exploitation may be tackled.
This work is of fundamental theoretical nature and is expected to produce general results on the important problem of the interaction between statistical learning and game theory. For concreteness, it will be tackled during the internship on the example of spam filter, but it is expected to have numerous ramifications and other applications: intrusion detection, fraud detection, etc.
URL sujet détaillé : http://www.eurecom.fr/~loiseau/Internship_EURECOM_SpamFilter.pdf
Remarques : A possibility may be offered to continue with a PhD.
Remuneration can be given if the student needs it.
|
|
|
|
|
|
SM207-64 Resource allocation in data centers
|
|
|
Description
|
|
Background:
With the prominent cloud-computing paradigm, most jobs corresponding to web services, enterprise software, social-network services, etc. are now executed within virtual machines (VM) running on physical servers located in data centers. Each physical server can host a potentially large number of VMs. In the last few years, an important research activity has emerged on VM allocation, to address the question: on which physical server should each VM be run?
An important aspect that has been particularly discussed is the energy consumption. Indeed, the energy consumed by data centers constitutes a significant fraction of the world's energy consumption and represents a large part of the cost of running the data center [1,2]. To reduce energy consumption, various mechanisms have been proposed which all consist in turning off servers or network equipment at times of low usage [3]. As a result, in the VM allocation, VMs corresponding to the same job should be placed on the same physical server in order to turn the others off. However, this type of allocation is not good in terms of reliability [4]. Indeed, if all VMs of a job are on the same physical server (or in the same cluster), then the job is extremely sensitive to failure of this server (or cluster).
Objectives of the internship:
The goal of this internship is to develop a VM allocation policy that minimizes energy consumption while respecting constraints of reliability. To be realistic, we will consider a dynamic scenario with random arrivals of jobs and a probabilistic model of failure for each component. After a short literature survey on VM allocation, the student will formulate the allocation problem as an optimization problem under probabilistic constraints. He/she will search if an optimal allocation policy can be found and look into its fundamental properties. He/she will then perform numerical evaluations using realistic data-center topologies.
This work will allow studying the trade-off between the guaranties of reliability that can be offered to customers of the data centers and the reduction of energy cost that can be achieved.
Besides the application to reliability in data centers, the problem of resource allocation under probabilistic constraints is a fundamental interest. This work will have many ramifications (e.g., the development of distributed allocation mechanisms for large scale networks) as well as many other applications (e.g., as bandwidth allocation in virtual networks).
References:
[1] J. M. Kaplan, W. Forrest, and N. Kindler. Revolutionizing data center energy efficiency. Technical report, McKinsey & Company, July 2008.
[2] N. El-Sayed, I. A. Stefanovici, G. Amvrosiadis, A. A. Hwang, and B. Schroeder. Temperature management in data centers : why some (might) like it hot. In Proceedings of ACM SIGMETRICS/Performance, pages 163=96174, 2012.
[3] M. Lin, A. Wierman, L. Andrew and E. Thereska. Dynamic right-sizing for power-proportional data centers. IEEE Transactions on Networking, 2013 (to appear).
[4] P. Bod=EDk, I. Menache, M. Chowdhury, P. Mani, D. A. Maltz, and I. Stoica. Surviving failures in bandwidth-constrained datacenters. In Proceedings of the ACM SIGCOMM, pages 431=96442, 2012.
URL sujet détaillé : http://www.eurecom.fr/~loiseau/Internship_EURECOM_reliability.pdf
Remarques : A possibility may be offered to continue with a PhD.
Remuneration can be given if the student needs it.
|
|
|
|
|
|
SM207-65 Economics of privacy in social networks
|
|
|
Description
|
|
Background:
The Internet advertisement industry weighted billions in the first half of 2012, a 14% increase over the same period in 2011 [1]. A large part of this amount is attributable to targeted advertisement, where advertisers use your private data to send advertisement that you are more likely to be interested in, and hence increase the likelihood that you buy the product. As a result, social networks (e.g., facebook) and web services (e.g., google) that collect information on users can make huge amounts of money simply by selling this information to advertisers.
This situation has led to a recent increase of the public awareness as witnessed in the medias, which also resulted in the start of an intense research activity around the development of privacy models and tools that allow users to gain control of their private data and potentially to sell them [1,2]. This brings two essential questions: how to put a price on each piece of data for the user? and of how much data to buy for the advertisers? Such questions started to be discussed recently [3] but are far from being well understood.
Objectives of the internship:
The goal of this internship is to build a game-theoretic model, which allows investigating the incentive of each user to sell his data. We will focus on the case of a social network, where private data of linked users are correlated (e.g., the age of friends are correlated) and try to understand how the position of a user in the social network impacts the value of his private data. After a short literature survey, the student will propose a model, compute the equilibria and try to find a structure in the equilibria relating to properties of the social network graph [4]. Simulations using real social network graphs or standard models (e.g., small world) may also be performed.
References:
[1] Interactive Advertising Bureau. http://www.iab.net.
[1] V. Erramilli. The Tussle around Online Privacy. IEEE Internet Computing, 16(4): 69-71, 2012.
[2] C. Riederer, V. Erramilli, A. Chaintreau, B. Krishnamurthy, P. Rodriguez. For sale : Your Data, By : You. In proceedings of HoteNets, 2011.
[3] A. Ghosh, A. Roth. Selling privacy at auction. In Proceedings of ACM EC, 2011.
[4] K. Bimpikis, O. Candogan, A. Ozdaglar. Optimal Pricing in Networks with Externalities. Operations Research, 60(4): 883-905, July-August 2012.
URL sujet détaillé : http://www.eurecom.fr/~loiseau/Internship_EURECOM_Privacy.pdf
Remarques : A possibility may be offered to continue with a PhD.
Remuneration can be given if the student needs it.
|
|
|
|
|
|
SM207-66 Représentations intermédiaires parallèles pour LLVM et GCC
|
|
|
Description
|
|
1. Sujet :
Application de la méthodologie SPIRE, développée au CRI et permettant l'extension des représentations intermédiaires de compilateurs, aux plateformes LLVM et GCC.
2. Projet :
La plupart des grandes plateformes de compilation comme LLVM, GCC ou PIPS ont été conçues dans l'optique de la génération de code pour des langages impératifs séquentiels. Avec la multiplication des architectures multicoeurs, des langages explicitement parallèles de type X10, Habanero-Java... et des extensions parallèles type OpenMP et MPI, il convient d'envisager d'étendre l'architecture de ces plateformes pour être à même de traiter les spécificités de ces langages. Afin de pouvoir réutiliser autant que possible l'investissement logiciel lourd auquel correspondent ces compilateurs, la méthodologie SPIRE d'extension "légère" de représentation intermédiaire, une structure de données centrale dans ces systèmes, a été proposée au CRI et validée, en partie, dans le cas de la plateforme de compilation PIPS.
3. Descriptif :
L'objet du stage de niveau Master 2 Recherche, de quelques mois, est, en partant du système SPIRE développé par le CRI :
- d'étudier en détail les représentations intermédiaires (RI) des compilateurs LLVM et GCC ;
- d'analyser les extensions parallèles des RIs déjà introduites dans la littérature ;
- de tester la capacité de la méthodologie SPIRE à étendre ces RIs séquentielles au monde parallèle ;
- et d'implémenter dans au moins une de ces plateformes ces RI étendues pour en tester expérimentalement la pertinence.
4. Exigences :
Une bonne connaissance de la programmation en C, des systèmes de compilation et des méthodes de spécification formelle est nécessaire.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-67 Proposer des modèles énergétiques réalistes pour les infrastructures et les services de Clouds
|
|
|
Description
|
|
Contexte :
Ce sujet s'inscrit dans le contexte des travaux de l'équipe Myriads sur l'efficacité énergétique dans les systèmes distribués à grande échelle. L'équipe Myriads s'intéresse en particulier aux infrastructures virtualisées ou Clouds. Il s'agit d'améliorer l'efficacité énergétique de ces infrastructures en mettant en óuvre des politiques de gestion de ressources qui répondent à la fois à des besoins de performances et d'efficacité énergétique. L'équipe Myriads accorde beaucoup d'importance à la validation expérimentale des systèmes issus de ses travaux de recherche. A cette fin, elle utilise la plate-forme d'expérimentation Grid'5000 (http://www.grid5000.fr) et collabore avec des partenaires académiques et industriels fournissant des cas d'études réalistes pour la validation des prototypes réalisés.
Mission :
Les infrastructures distribuées et parallèles offrent aux utilisateurs des capacités de calcul considérables. Elles reposent sur des ressources de calcul distribuées reliées par des réseaux. Leur élaboration nécessite la conception d'algorithmes et de protocoles pour gérer ces ressources de manière transparente pour l'utilisateur.
Récemment, la maturité des techniques de virtualisation a permis l'émergence d'infrastructures virtualisées (Cloud). Ces infrastructures fournissent aux utilisateurs des ressources de manière dynamique, fiable et adaptée à leurs besoins. En bénéficiant des économies d'échelle, ces infrastructures distribuées peuvent gérer efficacement leurs ressources et offrir des capacités de stockage et de calcul quasiment illimitées tout en minimisant les coûts pour les utilisateurs. Cependant, la rapide expansion de ces infrastructures conduit à une augmentation inquiétante et non maîtrisée de leur consommation électrique. Ces travaux ont pour objectif la compréhension fine de la consommation énergétique des ressources de Clouds aux niveaux microscopique et macroscopique.
Mesurer la consommation énergétique des infrastructures distribuées est une opération complexe de par la nature multi-échelle et hétérogène de ces systèmes et du fait que ces ressources sont géographiquement dispersées. La consommation peut en effet être mesurée pour toute l'infrastructure, pour une machine de calcul ou pour un cóur par exemple.
Passer ensuite de l'instrumentation à la modélisation est une étape ardue et pourtant indispensable pour pouvoir améliorer l'efficacité énergétique de telles infrastructures. Il est en effet essentiel de comprendre comment l'électricité est consommée pour être en mesure de concevoir des politiques d'économies d'énergie.
La plupart des modèles présentés dans la littérature décomposent la consommation d'une machine en la consommation de chacun de ses composants [1] ou considèrent que la consommation est proportionnelle à l'utilisation [2]. Cependant, nous avons montré les limites de ces deux approches dans [3]. Quant aux approches expérimentales présentes dans la littérature, elles ne concernent en général qu'une architecture de machine, voire qu'une application type. Ainsi, il est nécessaire de concevoir de nouveaux modèles plus proches de la réalité.
Concernant la consommation d'infrastructures entières, certaines études montrent que les machines

de calcul représentent la plus grosse part dans la consommation des Clouds [4], alors que d'autres études montrent que, suivant les cas d'utilisation, le coût énergétique du réseau qui relie l'utilisateur aux ressources de calcul peut être supérieur au coût énergétique des machines [5]. La plupart de ces études n'ont pas la même définition du coût énergétique pour les infrastructures de Clouds : par exemple, le réseau d'accès utilisé par les utilisateurs n'est pas toujours pris en compte ainsi que les coûts liés à la climatisation. De même, certains travaux tiennent compte uniquement de la consommation dynamique des machines et non leur consommation fixe (consommation lorsque les machines sont allumées mais inutilisées).
Un autre problème ouvert : comment identifier la consommation liée à une application particulière ou une machine virtuelle donnée (en incluant les ressources impactés par cette utilisation telles que la climatisation et les ressources réseaux) ?
Description :
La première partie du travail consistera à modéliser finement les liens entre utilisation des différents composants d'une machine (CPU, NIC, RAM, disque) et consommation globale de la machine. Une étape de benchmarking sera donc incontournable. Ces benchmarks seront utilisés sur plusieurs modèles de machine différents pour démontrer leur généricité. La plate-forme Grid'5000 sera mise à contribution pour cette étape expérimentale puisque plusieurs clusters de cette plate-forme (offrant des architectures différentes) disposent de wattmètres. Les modèles énergétiques obtenus seront intégrés à l'outil SimGrid qui fournit des fonctionnalités de base pour la simulation d'applications distribuées hétérogènes sur des environnements distribués [6]. L'intégration à SimGrid se fera en collaboration avec deux partenaires de l'ANR SONGS (Simulation Of Next Generation Systems) : l'équipe AlGorille et l'équipe MESCAL.
Dans un second temps, ces modèles seront utilisés pour déterminer la consommation de services Clouds (comme GoogleDocs par exemple). Modéliser la consommation d'un service particulier requiert de considérer tous les composants impliqués depuis la machine de l'utilisateur (ordinateur ou client mobile) jusqu'au serveur utilisé dans le Cloud en incluant les réseaux qui les relient.
Enfin, ces modèles seront utilisés pour évaluer la consommation énergétique d'infrastructures entières. Il faudra pour cela ajouter à ces modèles les coûts énergétiques liés au stockage des données et à la climatisation notamment. En effet, la climatisation représente, dans le cas général, entre 30% et 50% de la consommation d'un centre de calcul. Il est donc indispensable d'intégrer son coût énergétique aux modèles développés pour que ceux-ci soient plus proche de la réalité et permettent de concevoir des politiques de gestion des ressources et des tâches de manière a effectivement économiser de l'énergie.
Références :
[1] "VMeter: Power modelling for virtualized clouds", Ata Bohra and Vipin Chaudhary,
IEEE International Symposium on Parallel & Distributed Processing (IPDPSW), 2010.
[2] "It's Not Easy Being Green", Peter Xiang Gao, Andrew Curtis, Bernard Wong, and S. Keshav, SIGCOMM 2012.
[3] "Demystifying Energy Consumption in Grids and Clouds", Anne-Cécile Orgerie, Laurent Lefèvre, and Jean-Patrick Gelas, Work in Progress in Green Computing (WIPGC) Workshop, in conjunction with the first International Green Computing Conference (IGCC), pages 335-342, 2010.
[4] "How dirty is your data?", Greenpeace report, 2011.
[5] "Green Cloud Computing: Balancing Energy in Processing, Storage and Transport", Jayant Baliga, Robert Ayre, Kerry Hinton, and Rodney Tucker, Proceedings of the IEEE, 99(1): 149-167, 2011.
[6] "SimGrid: a Generic Framework for Large-Scale Distributed Experiments", Henri Casanova, Arnaud Legrand, and Martin Quinson, IEEE International Conference on Computer Modeling and Simulation - EUROSIM / UKSIM, 2008.
URL sujet détaillé : http://www.irisa.fr/myriads/open-positions/internships/ploneexfile.2012-09-20.2417560408/attachment_download/file
Remarques : Équipe Myriads, IRISA, campus de Beaulieu, Rennes, http://www.irisa.fr/myriads
- Christine Morin christine.morin.fr
- Anne-Cécile Orgerie anne-cecile.orgerie.fr
Une poursuite en thèse est envisageable.
|
|
|
|
|
|
SM207-68 Outils pour analyser l'usage de Grid'5000 et pour aider à anticiper les pannes
|
|
|
Description
|
|
Contexte:
Ce sujet s'inscrit dans le contexte des travaux de l'équipe Myriads sur les systèmes distribués à grande échelle. L'équipe Myriads s'intéresse en particulier aux infrastructures virtualisées ou Clouds et fait partie de l'équipe de gestion de la plate-forme de recherche française Grid'5000 (http://www.grid5000.fr). Il s'agit d'améliorer l'efficacité énergétique et la tolérance aux fautes de ces infrastructures distribuées en mettant en óuvre des politiques de gestion de ressources qui répondent à la fois à des besoins de performances et d'efficacité énergétique. L'équipe Myriads accorde beaucoup d'importance à la validation expérimentale des systèmes issus de ses travaux de recherche. Ces validations s'appuient sur Grid'5000 et sur ses collaborations avec des partenaires académiques et industriels fournissant des cas d'études réalistes pour la validation des prototypes réalisés.
Mission:
Les infrastructures distribuées et parallèles offrent aux utilisateurs des capacités de calcul considérables. Comprendre l'usage de ces infrastructure est d'une importance capitale pour les dimensionner de manière adéquate (en terme de ressources de calcul, de stockage, réseau, air conditionné et approvisionnement électrique par exemple), ainsi que pour anticiper les pics de charge et donc les pannes et les goulets d'étranglement possibles.
Des analyses précédentes des logs de Grid'5000 ont montré que son usage est fortement hétérogène et qu'il est fait de pics et de creux d'utilisation [2, 3]. Cependant, l'usage global de Grid'5000 est comparable à l'usage de Grilles de calcul classiques [2, 4]. Ainsi, les outils développés dans le contexte de Grid'5000 devraient être adaptables à d'autres environnements de Grilles.
Tout d'abord, dans ce projet, nous nous attacherons à développer des outils pour détecter automatiquement les pannes et les erreurs, et ainsi aider à la gestion de ces pannes dans le cadre de la plate-forme Grid'5000. Ces outils auront pour but de catégoriser les pannes pour permettre le traitement automatique de certaines d'entre elles, facilitant ainsi l'administration de la plate-forme. Ces outils utiliseront les données disponibles sur la plate-forme tels que les traces d'utilisation. Il sera demandé d'analyser ces traces pour comprendre plus en détail l'utilisation de la plate-forme. Dans un deuxième temps, nous adapterons ces outils de prévision de pannes à la gestion de l'énergie dans les environnements de grilles. L'idée est d'être capable d'anticiper les pics de consommation électrique et les creux pour les ressources de calcul, de stockage, réseau et les infrastructures de refroidissement (ces dernières représentant à elles seules 30% à 50% de la consommation totale d'un centre de calcul).
Description:
Ce travail sera fondé sur une analyse en profondeur des traces d'utilisation de Grid'5000. L'analyse de traces peut avoir différents objectifs : surveillance de ressources [4], rapports d'utilisation [3], visualisation de l'utilisation [5], détection de motifs [6], estimation de la consommation énergétique [2], détection de pannes [5], etc.
Comme expliqué précédemment, dans notre contexte, les objectifs de cette analyse sont doubles : 1) anticiper les besoins en termes de ressources et de consommation électrique ; et 2) aider à la prise de décisions suite à une panne ou à un crash.
Ce projet requiert d'abord 1) de collecter les traces de la plate-forme (en utilisant les outils de surveillance déployés sur Grid'5000 tels que Monika et Ganglia) ; 2) d'analyser ces traces (à l'aide de méthodes statistiques par exemple) ; 3) de concevoir des outils de détection automatique (en temps réel et post-mortem) ; et 4) de valider ces outils en les déployant sur Grid'5000.
Les outils de détection utiliseront des techniques de traitement de données (data mining) et d'apprentissage (machine learning). Par exemple, ces techniques pourront être utilisées pour réaliser des profils d'utilisateurs typiques et de ressources typiques en terme d'utilisation. Des algorithmes temps réel et en différé seront utilisés pour les différents besoins de ce projet : analyse, prévision, ... Différents types de données seront utilisés pour cette analyse suivant leur disponibilité sur les différents sites de Grid'5000 : traces des réservations de ressources, historique des pannes, historique de l'utilisation du CPU, des disques, du réseau, mesures de consommation énergétique, etc.
Ce travail sera réalisé en collaboration avecn l'initiative INRIA nommée HEMERA [7] qui vise à expérimenter des problématiques à grande échelle, comme des algorithmes d'optimisation pour les grilles, d'étudier la robustesse des réseaux pair à pair ou des simulations dans le domaine de l'hydrogéologie ou de l'énergie.
Ce travail fera également l'objet d'une collaboration avec le Lawrence Berkeley National Laboratory (USA) dans le contexte du programme Inria. Cette collaboration portera plus particulièrement sur les outils d'apprentissage.
References:
[1] http://www.grid5000.fr
[2] Marcos Dias de Assunç=E3o, Anne-Cécile Orgerie, and Laurent Lefèvre, "An Analysis of Power Consumption Logs from a Monitored Grid Site", IEEE/ACM International Conference on Green Computing and Communications (GreenCom-2010), pages 61-68, 2010.
[3] Anne-Cécile Orgerie and Laurent Lefèvre, "A year in the life of a large-scale experimental distributed system: the Grid'5000 platform in 2008", INRIA Research Report RR-7481, 2010. [4] A. Iosup, C. Dumitrescu, D. Epema, Hui Li, and L. Wolters. "How are real grids
used? the analysis of four grid traces and its implications", IEEE/ACM
International Conference on Grid Computing (GRID), 2006.
[5] Lucas Mello Schnorr, Arnaud Legrand and Jean-Marc Vincent, "Detection and analysis of resource usage anomalies in large distributed systems through multi-scale visualization", Concurrency and Computation: Practice and Experience, Wiley, 2012
[6] Marcelo Finger, Germano C. Bezerra and Danilo R. Conde, "Resource use pattern analysis for opportunistic grids", International Workshop on Middleware for Grid Computing (MGC), 2008.
[7] https://www.grid5000.fr/mediawiki/index.php/Hemera
URL sujet détaillé : http://www.irisa.fr/myriads/open-positions/internships/ploneexfile.2012-09-20.2417560408/attachment_download/file
Remarques : Équipe Myriads, IRISA, campus de Beaulieu, Rennes, http://www.irisa.fr/myriads
- Christine Morin christine.morin.fr
- Anne-Cécile Orgerie anne-cecile.orgerie.fr
Une poursuite en thèse est envisageable.
|
|
|
|
|
|
SM207-69 Une bibliothèque réelle unifiée pour Coq
|
|
|
Description
|
|
Il existe plusieurs bibliothèques de nombres réels dans Coq et de nombreux travaux ont été et sont encore menés sur la formalisation des nombres réels dans Coq. Ce stage concerne les deux principales bibliothèques, la bibliothèque standard classique "Reals" [1] et la bibliothèque intuitionniste "CoRN" [2]. Une étude de ces deux bibliothèques a été faite par leurs auteurs (Mayero-Niqui) afin de développer une unique bibliothèque des nombres réels qui comprendrait une partie commune [3]. Le but de ce stage est de poursuivre cette étude, dont les conclusions ne sont pas figées, ainsi que le développement (un prototype existe).
Ce sujet requiert une bonne connaissance de Coq, de la théorie des types, du calcul des construction inductives et de l'analyse réelle classique et intuitionniste.
Ce sujet pourra également aborder la problématique de l'extraction de programme [4] et de la réalisabilité classique [5].
[1] http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual005.html
[2] http://corn.cs.ru.nl/
[3] M.Mayero. Manuscrit d'habilitation à diriger des recherches. 2012.
[4] L. Cruz-Filipe and P. Letouzey. A Large-Scale Experiment in Executing Extracted Programs. Calculemus 2005.
[5] A.Miquel. Manuscrit d'habilitation à diriger des recherches. 2009.
URL sujet détaillé :
:
Remarques : Collaboration avec Bas Spitters:
http://www.cs.ru.nl/~spitters/
Séjours à Nijmegen (Pays-Bas) possibles.
Le sujet peut être étendu pour une éventuelle poursuite en thèse.
|
|
|
|
|
|
SM207-70 Reconstruction tomographique à partir de projections non-orientées
|
|
|
Description
|
|
La tomographie permet de reconstituer un objet (2D ou 3D) à partir d'un ensemble de projections de cet objet selon différents angles. Dans certaines applications (dont la cryo-tomographie électronique), les projections sont
acquises sans avoir d'information sur les angles de projection correspondant.Ce cas de figure a été largement étudié sans pour autant aboutir à une solution universelle. En
particulier, le cas (réel) de reconstruction d'objets déformables fait l'objet de recherche
actives. C'est un enjeu important car de nombreux objets étudiés actuellement par la tomographie sont en fait déformables.
Le cas de la tomographie où les projections sont orientées est déjà bien traité, mais le cas (qui
nous intéresse) où leurs orientations ne sont pas connues est traité actuellement par raffinement à
partir d'une première recontruction de l'objet. Cela ne rend que partiellement compte de la réalité et peut introduire des artefacts.
Dans ce cadre, nous proposons une nouvelle méthode de reconstruction, dans laquelle les angles des projections et l'objet sont reconstruits simultanément. La recherche de la solution se fait alors par optimisation globale dans l'espace des angles et de l'image.
Cette méthode est actuellement en développement (le cas statique binaire a été étudié à
Strasbourg dans la cadre de deux stages de master par C. Fillion en 2D, par N. Aubry en 3D). Le but de ce stage est d'étendre la méthode développé au cas des densités électroniques continues. L'idée est de s'inspirer du processus réel
en modélisant les atomes de la macromolécule par des sphères et l'acquisition au microscope par sa fonction de transfert.
Il faudra pour cela modifier la fonction de projection puis améliorer l'optimisation pour tenir compte de l'agrandissement l'espace de recherche.
Cette étude sera faite dans un premier temps en 2D sur des images simples générées artificiellement sans bruit puis en 3D.
URL sujet détaillé : http://lsiit-miv.u-strasbg.fr/miv/stages.php?sous_site_id=0
Remarques : co-encadrement : G. Frey
|
|
|
|
|
|
SM207-71 Décidabilité et Complexité en Logique de Séparation
|
|
|
Description
|
|
Parmi la variété d'approches et de techniques déployées pour l'analyse de spécifications en logique de séparation (model-checking, automates à compteurs, interprétation abstraite,..), l'approche par recherche de preuves apparaît peu développée.
Le but de ce sujet est donc de rechercher et d'identifier de nouveaux fragments décidables de la logique de séparation (avec et/ou sans extensions récursives et quantitatives), si possible moins restrictifs que le fragment purement existentiel, en utilisant une approche fondée sur la recherche de preuves et la construction de contre-modèles.
Voir sujet détaillé.
URL sujet détaillé : http://www.loria.fr/~galmiche/=stages/sujet1-M2R-2012.pdf
Remarques : Co-encadrement avec Daniel MERY
|
|
|
|
|
|
SM207-72 Sémantique des Phases Relationnelle et Elimination des Coupures pour Boolean BI
|
|
|
Description
|
|
Le but du sujet est de revisiter le théorème d'élimination des coupures de Boolean BI (BBI) par une approche fondée sur la sémantique des phases et les résultats de complétude forte d'Okada. Dans son
article sur le sujet Okada suggère que sa technique permet d'obtenir l'élimination des coupures de manière uniforme pour une grande variété de logiques. En définissant une sémantique des phases adaptée à BI, nous avons obtenu une preuve de l'élimination des coupures par cette approche sémantique. Un autre avantage de cette méthode est que la formalisation en Coq est relativement aisée.
L'objectif de ce travail est d'étudier cette méthode pour BBI.
Voir sujet détaillé.
URL sujet détaillé : http://www.loria.fr/~galmiche/=stages/sujet3-M2R-2012.pdf
Remarques : Co-encadrement avec Dominique LARCHEY-WENDLING
|
|
|
|
|
|
SM207-73 Tactiques de décision pour des structures non commutatives
|
|
|
Description
|
|
L'assistant de preuve Coq [1] permet de formaliser des résultats de plus en plus complexes, et ce grâce à la possibilité d'utiliser des tactiques de haut niveau pour résoudre des classes de buts pénibles, mais décidables (omega, ring, firstorder...).
Nous proposons dans ce stage d'étudier et d'implanter un algorithme de décision pour la logique linéaire cyclique (non-commutative) [2,3], ainsi que son fragment intuitionniste. L'intérêt principal d'une telle tactique réside dans un modèle particulièrement simple et répandu de ces logiques : les relations binaires.
Le stage aura deux composantes principales :
- l'étude et la définition d'optimisations ou de variantes de l'algorithme de décision (focalisation, élimination des symmétries, réduction de l'espace de recherche par typage, extension à d'autres opérateurs) ;
- l'implantation concrète de l'algorithme en OCaml, puis son intégration dans l'assistant de preuve Coq.
Des connaissances tant théoriques (logique linéaire, séquents, unification du premier ordre) que pratiques (programmation fonctionnelle, algorithmique) sont donc les bienvenues. Selon les goûts et intérêts du stagiaire, le stage pourra évoluer plus du côté logique linéaire, plus du côté programmation OCaml, ou plus du côté Coq.
[1] http://coq.inria.fr
[2] David N. Yetter, Quantales and (NonCommutative) Linear Logic, Journal of Symbolic Logic, Vol. 55, No 1, pp 41-64 (1990)
[3] V. Michele Abrusci, Phase Semantics and Sequent Calculus for pure non Commutative Classical Linear Propositional Logic, Journal of Symbolic Logic, Vol. 56, No 4, pp 1403-1451 (1991)
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-74 Formalisations du pi-calcul en Coq
|
|
|
Description
|
|
L'objectif du stage est d'étudier des techniques introduites récemment pour formaliser dans l'assistant à la preuve Coq la théorie opérationnelle du pi-calcul.
Le pi-calcul est un formalisme pour la spécification et l'analyse des systèmes concurrents introduit par R.Milner (cf. [1,2]). Il fournit une syntaxe dans laquelle décrire de tels systèmes comme des processus, qui interagissent entre eux suivant une topologie de communication pouvant évoluer au cours du temps. Le raisonnement sur les propriétés exprimées par de tels processus se fait souvent en termes d'équivalence: on souhaite établir que deux processus, bien que "codés" de manière différente, expriment essentiellement le même comportement. Des preuves d'équivalences, si elles sont formalisées à l'aide d'un outil tel que Coq [3], fournissent des garanties sur des systèmes parallèles, objets sur lesquels il est notoirement difficile de raisonner de manière rigoureuse.
Tout en étant fondé sur un langage concis, le pi-calcul a un grand pouvoir expressif, et sa définition formelle fait intervenir un certain nombre de subtilités techniques qui sont sources de complications dans le cadre d'une formalisation. Parallèlement à cela, les preuves d'équivalences entre processus sont rapidement des objets difficiles à manipuler en Coq, du fait de leur grande taille. Le but de ce stage est de mettre en oeuvre des méthodes récemment développées afin de faciliter à la fois la formalisation du pi-calcul et la construction de preuves d'équivalences comportementales entre processus.
Ces travaux s'inscrivent dans deux directions complémentaires: sur un plan pratique, il s'agit de faire progresser la capacité à raisonner formellement sur les programmes concurrents. D'un point de vue plus théorique, il s'agit de contribuer à dégager des abstractions utiles pour la présentation et l'étude métathéorique des calculs de processus.
[1] R. Milner, Communicating and Mobile Systems: the Pi-Calculus, Cambridge University Press
[2] M. Hennessy, A Distributed pi-calculus, Cambridge University Press
[3] http://coq.inria.fr
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-75 Algèbres de Kleene, automates et expressions régulières
|
|
|
Description
|
|
Nous proposons d'étudier dans ce stage différentes extensions des algèbres de Kleene (dont les modèles principaux sont les automates et les expressions régulières), du point de vue de leur décidabilité. L'objectif à long terme est la définition en Coq [1] de tactiques de décisions: pour les relations binaires, pour l'arithmétique quantifiée, etc...
Nous prendrons comme point de départ les algèbres de Kleene avec converse, dont la théorie équationelle est théoriquement décidable [2], mais dont le seul algorithme connu à ce jour a une complexité trop élevée pour être utile en pratique. Nous nous intéresserons donc à améliorer cet algorithme, voire à en trouver un meilleur.
Une autre extension que nous considèrerons correspond aux algèbres d'actions [3], dont la décidabilité de la théorie équationelle est toujours une question ouverte. Cette extension a de très bonnes propriétés mathématiques, et sa décidabilité serait très utile en pratique, notamment au sein d'un assistant de preuve.
Le stage aura donc une forte composante théorique et algorithmique (compréhension des notions algébriques mises en jeu et des algorithmes sous-jacents); il pourra éventuellement se prolonger par une composante implémentatoire, dans un langage de programmation lambda, voire dans l'assistant de preuve Coq.
[1] http://coq.inria.fr
[2] S. L. Bloom, Z. Esik, et Gh. Stefanescu, Notes on equational theories of relations. Algebra Universalis, 33 (1995) 98-126
[3] V.R. Pratt, Action Logic and Pure Induction. LNCS 478, 97--120, Springer-Verlag, 1990.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-76 Workflows Scientifiques sur les Clouds
|
|
|
Description
|
|
Les workflows sont une méthode pour formaliser et structurer les calculs scientifiques. Ils sont utilisés par un grand nombre de projets qui travaillent sur des grands ensembles de données (Montage, LHC Atlas, etc.) et qui nécessitent un grand ensemble de ressources (Clusters, SuperCalculateurs, Grilles).
Pour le moment, il n'est pas aisé d'utiliser des workflows dans le cadre du Cloud Computing. Pour autant, de part la forte augmentation de ressources disponibles via les différents Clouds, les workflows ont tous intérêts à en tirer parti.
Le but de ce stage sera d'étudier et de proposer des algorithmes d'ordonnancement pour optimiser (coût et performance) l'utilisation des Clouds par les workflows scientifiques. Les algorithmes développés seront testés par simulation via le projet ANR INFRA SONGS (http://infra-songs.gforge.inria.fr/).
URL sujet détaillé :
:
Remarques : Co-encadrement: Frédéric Desprez
|
|
|
|
|
|
SM207-77 Reconstruction par simplification homologique
|
|
|
Description
|
|
À partir d'un nuage de points censé échantillonner un objet (obtenu par exemple avec un scanner), on cherche à reconstruire un maillage ayant la même topologie que l'objet (pas de composante connexe volante, de petite boucle, etc). Des méthodes développées ces dix dernières années permettent de calculer cette topologie sans faire d'hypothèses très fortes sur l'objet ou les points. Transformer l'algorithme qui fait ce calcul en un algorithme de reconstruction est difficile, la reconstruction étant NP-dure. L'objectif du stage est d'étudier un cas particulier de complexité polynomiale, sous des points de vue algorithmiques, théoriques et expérimentaux.
URL sujet détaillé : http://geometrica.saclay.inria.fr/team/Marc.Glisse/stage/homological-simplification/
Remarques :
|
|
|
|
|
|
SM207-78 Population Dynamics as the Limit of Finite Interaction Models
|
|
|
Description
|
|
One of the main challenges in the field of population dynamics is to derive the governing dynamics of an evolving population (replicator dynamics, Lotka-Volterra, etc.) as the mean field limit of a spatial interaction model where the individuals making up the population interact at an atomic level. Heuristically, it is usually assumed that these atomic pairwise interactions give rise to an average population behavior that follows the population dynamics under question, but this is not always the case. In fact, depending on the interaction graph between the population's atoms, one might witness critical percolation-like phenomena leading to a behavior which is radically different from what one observes in standard population models. As such, the object of this internship will be to study game-like interactions of players over large (not necessarily complete) random graphs, and to derive the system's steady states in the limit where the size of the population becomes asymptotically large.
Prerequisite mathematical background: Game Theory, Dynamical Systems, Probability (a background in statistical physics would be helpful but is not required)
References:
- [Du99] R. Durrett: Stochastic spatial models, SIAM Review 41 (1999) 677-718. MR2000h:60086
- [NoMay92] M.A. Nowak and R.M. May: Evolutionary games and spatial chaos, Nature 359 (1992), 826-829
- [NoMay93] M.A. Nowak and R.M. May: The spatial dilemmas of evolution, Int. J. Bifur. Chaos Appl. Sci. Engrg. 3 (1993), 35-78. MR 94c:92014
URL sujet détaillé :
:
Remarques : Co-encadrement avec Panayotis Mertikopoulos.
Possibilité de rémunération. Possibilité de poursuite des travaux en thèse.
|
|
|
|
|
|
SM207-79 Learning Dynamics for Concave Games
|
|
|
Description
|
|
The vast majority of learning algorithms and dynamics for game theory have focused on finite games and mixed extensions thereof. However, in many practical applications of game theory (Cournot oligopolies in economics, routing and congestion problems in wireline networks, power control in wireless networks, etc.), the games under consideration are not finite and the standard approaches do not apply. One of the main difficulties that arises in this much more general class of quasi-concave games (games with convex action sets and quasi-concave utility functions), is that learning algorithms/dynamics must intrinsically respect the structure of the game's action space and its convexity constraints. Accordingly, the object of this internship will be to study systematic ways of transforming the game's action space (either by changing its geometry or by mapping the problem to an unconstrained one) in a way that allows one to write consistent and distributed dynamics for learning and optimization, and to then examine the properties of these dynamics with respect to the solution concepts of the underlying game.
Prerequisite mathematical background: Game Theory, Dynamical Systems, Convex Analysis (a background in differential geometry will be very helpful but it is not required)
References:
- [ABB04] F. Alvarez, J. Bolte, and O. Brahic, Hessian Riemannian gradient flows in convex programming, SIAM Journal on Control and Optimization, 43 (2004), pp. 477=96501.
- [HS03] J. Hofbauer and K. Sigmund, Evolutionary game dynamics, Bulletin of the American Mathematical Society, 40 (2003), pp. 479=96519.
URL sujet détaillé :
:
Remarques : Co-encadrement avec Panayotis Mertikopoulos.
Possibilité de rémunération.
Possibilité de poursuite des travaux en thèse.
|
|
|
|
|
|
SM207-80 Many discrete event systems (DES) arise as formal models of real-world system that are only partially observable. In this case , one deals with la- beled transition systems, typically
|
|
|
Description
|
|
Many discrete event systems (DES) arise as formal models of real-world
system that are only partially observable. In this case , one deals with la-
beled transition systems, typically =0Cnite, where the labeling is partial and
non-injective. When particular non-observable transitions are of crucial in-
terest, such as faults, the problem arises to determine whether or not such
an event has occurred, based on the sole information of the observable behavior ; this is known in the literature as the diagnosis problem for DES. The
case of stochastic DES has been addressed thus far by relatively few authors, and essentially under a language theo-
retic viewpoint that makes few use of properly probabilistic techniques. The goal of the internship is to develop a probabilistic approach to diagnosis, with emphasis on the exploitation of an underlying Markovian system, and
the development of diagnosis criteria based on statistic sampling/testing methods ; background knowledge and interest in probability theory, stochastic processes or mathematical statistics are thus prerequisites for this internship.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/m2-13-sth.pdf
Remarques :
|
|
|
|
|
|
SM207-81 Petri net unfolding methods for verifying weak properties
|
|
|
Description
|
|
D=B4escription du stage:
Petri nets and their partial order unfoldings have been increasingly used in the field of control for discrete event systems, in particular for fault diagnosis.
This task (in its event-based form) can be resumed as follows: given a system that is only partially observable - i.e. only some of its transitions carry an observable label -, deduce from the observable behaviour whether or not a certain unobservable transition f - the fault - has occurred. The associated question of
diagnosability asks if the system satisfies the following : after the occurrence of f, only a bounded number of additional events is possible before the observation allows to unambiguously deduce the occurrence of f. In recent work , it was shown that the concurrent behaviour of concurrent systems - modeled by Petri nets - can exhibit a weaker form of diagnosability.
There, a system is called weakly diagnosable if the fault is discovered on all progressive behaviours, i. e. under the additional condition that all the different local subprocesses of the distributed system under study progress in an
equitable manner, and no enabled transition remains enabled indefinitely without firing. The traditional strong diagnosability property cited above implies weak diagnosability, and both are equivalent in the case of sequential systems. Weak diagnosability constitutes a genuinely concurrency-based problem for Petri net analysis. The purpose of the internship is to develop
- adequate finite complete prefixes of Petri net unfoldings that
suffice for checking weak diagnosability, and
- efficient algorithms for the construction of these prefixes and
the fast verification of weak diagnosability.
Depending on the candidat's interest and background, it is possible- yet not mandatory - to study extensions to further properties and/or more general model
classes.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/m2-13-sth.pdf
Remarques :
|
|
|
|
|
|
SM207-82 Computer algebra for constant-size geometric problems
|
|
|
Description
|
|
Various conjectures in discrete and computational geometry involve small sets of elementary geometric primitives. For example, the width of a planar convex set is the smallest possible distance between two parallel lines enclosing the set. It is conjectured that if a convex set contains no triangle of width more than 1 then that convex set has width at most the golden ratio (1+sqrt(5))/2.
The goal of this internship is to tackle this type of conjectures using tools from computer algebra.
A candidate geometric configuration violating the conjecture can easily be described as a vector (x1 , ... , xn ) ∈ R^n satisfying a system (S) of polynomial equalities and inequalities of the form:
f1(x1 , ..., xn) = 0, . . . , fk(x1 , ..., xn) = 0
g1(x1 , ..., xn)> 0, . . . , gp(x1 , ..., xn)> 0
Settling the conjecture thus amounts to show that (S) has no real solution or to exhibit a solution that provides a counter example.
General algorithmic methods such as subdivision methods or critical point methods, can decide whether a given polynomial system has real solutions. In the worst-case they have exponential time complexity. In practice, they are sensitive to various properties of the system (the ambient dimension for subdivision techniques, singularities for the critical point methods), so each method has its own strengths and weaknesses and often needs to be tailored to the problem at hands.
During this internship, the candidate will get acquainted with different polynomial solving methods and will explore modelings of discrete geometry problems. Depending on the interests of the candidate, this internship can also lead to the development of specific extensions of computer algebra libraries.
URL sujet détaillé : http://webloria.loria.fr/~moroz/internships/computer_algebra_geometric_problems.pdf
Remarques : Co-encadrement: Xavier Goaoc et Guillaume Moroz.
|
|
|
|
|
|
SM207-83 Machines de Mealy et problème de Burnside
|
|
|
Description
|
|
Un automate avec une bande d'entrée et une bande de sortie peut être vu comme une machine transformant un mot d'entrée en un mot de sortie. En faisant varier l'état d'entrée de l'automate, on obtient un ensemble d'applications sur les mots, et on peut s'intéresser au semi-groupe engendré par ces applications, voir au groupe sous certaines conditions. On peut ajouter de la structures sur un tel automate, en imposant que les applications induites par les états (resp. les lettres) sur les lettres (resp. les états) soient des permutations, on parle alors d'automate inversible (resp. réversible); voire que l'inverse d'un tel automate ait également ces propriétés-là, on parle alors d'automate biréversible.
Rostislav Grigorchuk a donné un exemple d'automate qui engendre un groupe solution du problème de Burnside (groupe infini finiment engendré dont tous les éléments sont d'ordre fini). Cet automate est juste inversible.
Le but de ce stage est de déterminer s'il existe un automate biréversible répondant au problème de Burnside.
URL sujet détaillé : http://www.liafa.univ-paris-diderot.fr/~picantin/mealym.html
Remarques : Stage indemnisé selon dispositions réglementaires.
Possibilité de poursuite en thèse, financée par
l'ANR JCJC MealyM.
Le stage a lieu au sein d'un groupe actif sur le sujet composé de trois chercheurs ou enseignants-chercheurs permanents et un post-doc.
|
|
|
|
|
|
SM207-84 Prédicats exacts pour la génération de maillages
|
|
|
Description
|
|
Ce sujet de stage de Master concerne la mise au point de nouvelles méthodes de génération de maillages, pour la simulation numérique et le graphisme par ordinateur, dans le cadre du projet GOODSHAPE (l'un des premiers projets soutenus par le Conseil Européen de la Recherche).
Le sujet concerne l'étude d'une méthode de génération de maillages fondée sur la notion de diagramme de Voronoi barycentrique, qui permet d'optimiser la distribution des points et la forme des triangles. L'algorithme sous-jacent fait appel à des calculs d'intersections, qui peuvent rencontrer des situations dégénérées (par exemple des tangences, parallelisme, ...) Le stage concerne la mise au point d'une méthode de perturbartion symbolique, permettant de traiter efficacement ces situations dégénérées.
Objectifs du stage:
* comprendre la définition d'un diagramme de Voronoi restreint et de la méthode de perturbation symbolique "Simulation of Simplicity" (c.f. références biblio sur la page web du sujet)
* mise au point d'un schéma de perturbation symbolique pour les prédicats mis en jeu dans le calcul du diagramme de Voronoi restreint
* (optionnel) implantation en C++ de l'algorithme dans le logiciel "Graphite" de l'équipe et application à des problèmes de re-maillage
Compétences à avoir:
* Algèbre et géométrie de base
* (optionnel) langage C++
URL sujet détaillé : http://alice.loria.fr/index.php/positions/8-master/64-flexible-mesh-generation.html
Remarques : Le stage est rémunéré
Possibilités de poursuivre en thèse
|
|
|
|
|
|
SM207-85 Shape synthesis for hand controllers
|
|
|
Description
|
|
This internship considers the automatic synthesis of the shape of controllers to better fit the hand and wishes of a user. More specifically, starting from a 3D capture of the hand of the user in a specific pose, the system automatically generates the shape of a mouse, joystick, or pad. The end goal is to synthesize and print a shape that can be fixed on an existing device, replacing the original design, or to create an entirely new device.
The internship has two main parts: Acquiring the pose of the user's hand, as well as synthesizing the shape of the controller. Possible approaches for the first part include the use of cameras, markers, or specialized devices such as a depth camera (available in our lab). The second objective requires the proper formulation as a shape optimization problem, inspired by techniques from geometry and topology optimization, as well as by-example synthesis techniques. We will print and test the results on our 3D printer.
The internship will be co-supervised by Sylvain Lefebvre and Rhaleb Zayer and will take place within the ALICE team of INRIA Nancy Grand-Est. This project is part of the ERC ShapeForge and, if successful, could be pursued by a PhD within our team.
URL sujet détaillé : http://webloria.loria.fr/~slefebvr/teaching/topics/2012-controller-synth.pdf
Remarques : - Co-encadrement avec Rhaleb Zayer (INRIA Nancy)
- Possibilité de rénumération
|
|
|
|
|
|
SM207-86 Processus d'allocations dans les jeux coopératifs
|
|
|
Description
|
|
Ce stage se situe en théorie des jeux coopératifs, ils est naturellement pluridisciplinaire (mathématiques, informatique, économie).
En théorie des jeux coopératifs, une règle d'allocation distribue pour chaque situation envisageable une ressource entre des individus en conflit.
Shapley [1953] propose un ensemble d'axiomes qui permet de caractériser une règle d'allocation, connue sous le nom de valeur de Shapley.
Ces axiomes incorporent un principe d'optimalité, des principes d'équité et un principe d'additivité du processus d'allocation.
Plus récemment, Hamiache [2001] propose une interprétation dynamique: Il introduit un système dynamique sur l'ensemble des jeux, et la valeur de Shapley d'un jeu apparaît comme (une projection de) l'attracteur atteint par ce système dynamique, en prenant pour condition initiale le jeu donné.
L'objectif de ce stage est double :
1) Dans un premier temps: s'approprier cette méthode dynamique de construction ;
en effet, si la preuve d'Hamiache est formellement correcte, les idées et et les concepts
sous-jacents restent à éclaircir.
2) Ensuite : étudier la possibilité d'adapter la démarche à d'autres règles d'allocation classiques.
Bibliographie :
Matrix analysis for associated consistency in cooperative game theory
Genjiu Xu a,b,∗, Theo S.H. Driessen b, Hao Sun
Linear Algebra and its Applications 428 (2008) 1571=961586
Associated consistency and Shapley value
Gérard Hamiache
Hamiache G. Int J Game Theory (2001) 30:279=96289
A MATRIX APPROACH TO THE ASSOCIATED CONSISTENCY WITH AN APPLICATION TO THE SHAPLEY VALUE
Hamiache G. International Game Theory Review, Vol. 12, No. 2 (2010)
A dynamic approach to the Shapley value based on associated games
Yan-An Hwang, Jie-Hau Li and Yaw-Hwa Hsiao
nt J Game Theory (2005) 33: 551=96562
Shapley LS (1953) A Value for n-Person Games. In: Kuhn HW, Tucker AW (eds) Contributions
to the Theory of Games II, Annals of Mathematics Studies Vol. 28. Princeton University
Press, Princeton NJ pp. 307=96317
URL sujet détaillé :
:
Remarques : ce stage sera co-encadré par Philippe Solal. Professeur d'économie à l'université de St-etienne
|
|
|
|
|
|
SM207-87 Extensions of the Grid Exclusion Theorem
|
|
|
Description
|
|
The parameter of treewidth can be seen as a measure of the topological resemblance of a graph to the structure of a tree. Treewidth has been a cornerstone concept of the Graph Minors Project, developed by Robertson and Seymour, has been one of the most powerful and widely used tools in modern Algorithmic Graph Theory, and has numerous applica- tions in diverse fields such as Artificial Intelligence, Theory of Programming Languages, Database Theory, and Distributed Computing.One of the most influential results of the Graph Minors Project is the following:
Grid Exclusion Theorem (GET): There exists a function f : N → N such that every graph G
with treewidth at least f(k) contains a (k =D7 k)-grid as a minor.
A quite technical proof of the GET appeared, for the first time, in the 5th paper of the Graph Minors series. Another, still quite complicated, proof appeared later where f(k) = 400^k^5. Moreover a polynomial lower bound was given for f by showing that there are graphs excluding a (k =D7 k)-grid as a minor that have treewidth Ω(k2 log k) and was conjectured that the function f can be made polynomial.
The GET gave rise to a great variety of algorithmic applications on graph problems. In general, most of them are based to the fact that if the problem input has a grid-minor, this can serve as a YES/NO-certificate for the problem and thus immediately provide an answer to it, while if the treewidth is small, the problem can be solved using dynamic programming techniques. As the efficiency of this simple win/win approach depends heavily on the function f, it is imperative that better (preferably polynomial) bounds are obtained, even for special graph classes. In fact, it has been proved that the function f in the GET can become linear if we restrict G to belong in a graph class excluding some fixed graph as a minor.
Results and methodologies as those described above gave rise to what is now known as Bidimensionaliy Theory. This is a general meta-algorithmic theory with a wide range of applications such as sub-exponential parameterised algorithms, approximation algorithms/schemes, and kernelization algorithms. However, the potential of this theory is limited to classes where f can be proved to be polynomial or for cases where different types of YES/NO-certificates can be defined. Such a different certificate would be provided by resolving the following conjecture:
Conjecture: There exists a function g : N =D7 N → N such that every graph G with treewidth at least g(k, r) contains as a minor k disjoint copies of the (r =D7 r)-grid. Moreover, the function g(k, r) is polynomial on k.
Notice that if the above conjecture holds, then a set of disjoint copies of small grids could still provide either a YES/NO-certificate or (polynomially) small treewidth for applying dynamic programming. That way, the above conjecture could serve as the combinatorial base for a vast extension/revision of bidimensionality theory. Moreover, as this conjecture is actually a gener- alisation of GET, it can also provide valuable insight towards resolving the general question on where GET holds for some polynomial f.
URL sujet détaillé : http://www.lsi.upc.edu/~sedthilk/stage/stage_2013_Thilikos.pdf
Remarques :
|
|
|
|
|
|
SM207-88 Analyse et conception d'un système de vote
|
|
|
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 sujets à des attaques, comme un bourrage d'urne massif~[1].
L'objectif de ce stage est de concevoir un protocole de vote hybride, utilisant le papier pour les électeurs mais comportant des informations lisibles par une machine (e.g. codes à barre) pour faciliter le comptage.
Idéalement, ce protocole assurera la confidentialité du vote (même vis-à-vis de celui qui dépouille) ainsi que la vérifiabilité du vote (chacun peut vérifier après coup que son vote a été pris en compte).
On pourra en particulier s'inspirer des techniques développées dans le cadre du vote électronique.
URL sujet détaillé : http://www.loria.fr/~cortier/sujet-vote-2012.pdf
Remarques : Ce stage pourra être indemnisé. En particulier, ce stage a le support de la bourse Européenne ProSecure (ERC Starting Grant). Il pourra être poursuivi par une thèse.
|
|
|
|
|
|
SM207-89 Algorithme d'Ératosthène pour les polynômes irréductibles sur les corps finis.
|
|
|
Description
|
|
Équipe : CARAMEL
Problématique de recherche :
Le crible d'Ératosthène est un algorithme bien connu pour lister tous
les nombres premiers jusqu'à une certaine borne. De nombreuses
variantes théoriques ou pratiques existent, certaines relativement
récentes. Il existe de nombreuses similitudes entre l'anneau des
entiers et l'anneau des polynômes sur les corps finis. On s'intéresse
au problème similaire à celui résolu par le crible d'Ératosthène, mais
pour les polynômes irréductibles sur les corps finis, qui sont les
analogues des nombres premiers dans cette structure. Cette brique de
base sert dans de nombreux algorithmes liés à la théorie de
l'information, et en particulier en cryptographie. On peut par exemple
citer les algorithmes de crible pour résoudre le logarithme discret
dans les corps finis.
Sujet :
On s'intéresse plus particulièrement au cas des polynômes sur les corps
finis à 2 et 3 éléments, qui sont les plus pertinents pour la
cryptographie. L'objectif est de décrire, d'analyser et d'implanter un
algorithme analogue au crible d'Ératosthène pour lister tous les
polynômes irréductibles sur ces corps finis, jusqu'à une certaine borne
sur leur degré.
Lors de ce travail, le stagiaire devra :
- concevoir un algorithme pour les polynômes s'inspirant du crible
d'Ératosthène pour les entiers de manière à conserver la complexité
de l'algorithme mais en privilégiant une version qui utilise peu de
mémoire.
- implanter cet algorithme.
- explorer les optimisations algorithmiques du crible d'Ératosthène
et tester leur applicabilité dans le cas des polynômes.
Le développement se fera en langage C/C++ et s'appuiera sur une bibliothèque
développée dans l'équipe.
Bibliographie :
William F. Galway: Dissecting a Sieve to Cut Its Need for Space. ANTS 2000,
LNCS Volume 1838, 2000, pp 297-312.
A.O.L. Atkin, D.J. Bernstein, Prime sieves using binary quadratic forms,
Math. Comp. 73 (2004), 1023-1030.
URL sujet détaillé :
:
Remarques : co-encadrement avec Pierrick GAUDRY
|
|
|
|
|
|
SM207-90 Sécurité des protocoles cryptographiques
|
|
|
Description
|
|
Les protocoles cryptographiques visent à sécuriser les communications sur des réseaux ouverts comme Internet. À l'aide de primitives cryptographiques, ils permettent 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.
Dans ce cadre, des outils permettent d'analyser automatiquement la sécurité des protocoles.
Cependant, les outils ne permettent d'analyser qu'un seul protocole à la fois et sont trop lents pour analyser des protocoles de taille importante (explosion du nombre d'états).
Or les protocoles se décomposent souvent naturellement en plusieurs phases (authentification, établissement d'un canal confidentiel, etc.)
L'objectif de ce stage est d'étudier comment combiner les protocoles, en commençant par les protocoles d'authentification. Plus précisément, la question peut être formulée de la manière suivante : sous quelles conditions (hypothèses) un protocole d'authentification peut-il être utilisé par un autre protocole sans compromettre la sécurité de ce dernier ? On pourra s'appuyer sur des travaux effectués pour la composition des protocoles d'établissement de clefs.
URL sujet détaillé : http://www.loria.fr/~cortier/sujet-auth-2012.pdf
Remarques : Ce stage pourra être indemnisé. En particulier, ce stage a le support de la bourse Européenne ProSecure (ERC Starting Grant). Il pourra être poursuivi par une thèse.
|
|
|
|
|
|
SM207-91 Sécurité des protocoles cryptographiques
|
|
|
Description
|
|
Les protocoles cryptographiques visent à sécuriser les communications sur des réseaux ouverts comme Internet. À l'aide de primitives cryptographiques, ils permettent 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 visent à analyser la sécurité de ces protocoles. Deux grandes familles d'approches existent. D'une part, les modèles symboliques, relativement abstraits (utilisant par exemple des clauses de Horn ou des algèbres de processus) ont permis de développer des outils pour analyser automatiquement la sécurité des protocoles. À 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.
D'autre part, les modèles cryptographiques
sont basés sur la théorie de la complexité. Les messages sont
représentés par des suites finies de bits et les fonctions de chiffrement comme des algorithmes qui
opèrent sur ces suites. La question est alors de savoir si on peut construire un adversaire (une machine
de Turing) qui est capable, par exemple, d'apprendre une information confidentielle dans un temps
raisonnable (polynomial) et avec une probabilité non négligeable. Cette notion de sécurité semble
être plus adaptée pour identifier toutes les attaques possibles dans la réalité mais, en contrepartie, les
(lourdes) preuves de sécurité sont effectuées à la main et semblent difficilement automatisables
De nombreux travaux ont montré que ces deux types de modèles ne sont pas si dissemblables qu'il n'y parait : sous de bonnes hypothèses sur les primitives (chiffrement, ...) toute preuve de sécurité dans un modèle symbolique démontre en fait aussi la sécurité dans le modèle cryptographique.
L'objectif de ce stage est de poursuivre cette démarche avec une approche permettant d'analyser les primitives cryptographiques (chiffrement, ...) une à une. La première primitive étudiée sera le chiffrement, dans le cas de propriétés d'indistingabilité.
URL sujet détaillé : http://www.loria.fr/~cortier/sujet-soundness-2012.pdf
Remarques : Ce stage pourra être indemnisé. En particulier, ce stage a le support de la bourse Européenne ProSecure (ERC Starting Grant). Il pourra être poursuivi par une thèse.
|
|
|
|
|
|
SM207-92 Codes correcteurs et stéganographie adaptative
|
|
|
Description
|
|
La stéganographie est l'art de dissimuler un message de manière secrète dans un support anodin. La stéganalyse est l'art de déceler la présence d'un message secret. L'étude de la stéganographie/stéganalyse moderne a réellement débuté au début des années 2000.
Les codes correcteurs sont des outils importants pour la conception d'algorithmes pour la sténographie. Ils sont utilisés pour cacher des informations (le message secret) dans une image et également pour extraire l'information cachée à partir de l'image modifiée (F5-Hamming [Westfeld2001_F5], Modified Matrix Encoding : MME [Kim2007_MME], FastBCH [Zhang2009_BCH], [Sachnev2009_BCH], Reed-Solomon (RS) [Fontaine2009_BCH], ...). Par ailleurs, depuis peu, on admet que certains endroits de l'image sont plus sujets à détection, c'est à dire plus " sensible ", que d'autres [Fridrich2007_Embedding]. On modélise donc cette " sensibilité ", par une valeur de détectabilité attribuée à chaque pixel. L'insertion du message, à travers l'utilisation d'un code [Filler2011_STC], est alors effectuée avec la contrainte de minimisation de la somme des valeurs de détectabilité des pixels que l'on a modifiés. Ces valeurs peuvent être binaires, comme pour les algorithmes basés sur les wet-paper codes [Fridrich2005], ou bien dans un intervalle réel [Pevny_HUGO_2010], [Filler_MOD2011], [Kouider2012_ASO].
Dans ce stage, on s'intéresse au cas plus réaliste où les valeurs de détectabilité sont dans un intervalle réel. On appelle un algorithme qui prend en compte une telle contrainte un algorithme adaptatif et l'on parle de stéganographie adaptative [HUGO_2010], [Filler_MOD2011], [Kouider2012_ASO]. Le problème d'insertion adaptative est reconnu comme un problème intéressant de la stéganographie récente. Par ailleurs, le seul code existant pour le moment est le code de [Filler2011_STC]. Les propositions récentes [Pevny_HUGO_2010], [Filler_MOD2011], [Kouider2012_ASO], s'attachent, quant à elle, à la définition des valeurs de détectabilités plutôt qu'à l'aspect code correcteur.
Le stage se décomposera en deux parties: une première partie de compréhension du contexte de la stéganographie et de la steganalyse, ainsi que l'analyse des codes correcteurs d'erreurs utilisés dans les algorithmes non-adaptatifs (F5-Hamming [Westfeld2001_F5], Modified Matrix Encoding : MME [Kim et al. 2007], FastBCH [Zhang et al. 2009], [Sachnev et al. 2009], Reed-Solomon (RS) [Fontaine and Galand 2009], ...). La deuxième partie sera consacrée à l'analyse du code de [Filler2011_STC], utilisé dans les algorithmes adaptatifs, et à l'analyse de faisabilité d'adapter les codes correcteur utilisé dans les approches non-adaptatives pour les passer dans un mode adaptatif (éventuellement en choisissant un nouveau type de code correcteur).
URL sujet détaillé : http://www.lirmm.fr/~chaumont/SujetM2R_2012-2013-Steganographie_Codes.html
Remarques : Ce stage sera co-encadré par Anne-Elisabeth Baert et Eleonora Guerrini (enseignantes-chercheuses au LIRMM)
|
|
|
|
|
|
SM207-93 Round-to-Nearest HiPerf BLAS
|
|
|
Description
|
|
Motivation générale : Vers des BLAS à la fois précises et performantes
Les BLAS (Basic Linear Algebra Subroutines) constituent la couche logicielle de base dont dépendent la très grande majorité des bibliothèques et des applications de calcul scientifique. C'est ainsi qu'elles font l'objet de nombreux développements qui optimisent leurs vitesses de calcul selon les architectures matérielles visées : ATLAS, Goto BLAS, MKL, MAGMA BLAS, CuBLAS...
La précision de ces BLAS est l'autre enjeu, contradictoire mais justifié par la nécessité d'un calcul scientifique numériquement fiable et reproductible. Les X-BLAS permettent deux fois plus de précision grâce aux algorithmes double-double (DD). Ce doublement n'est parfois pas suffisant. MPACK est un exemple de BLAS arbitrairement précise basées sur les bibliothèques génériques de multi-précision GMP, MPFR, ou encore QD/DD.
Objectif du stage :
Des algorithmes récents permettent la meilleure précision possible de la somme de n flottants, et donc du produit scalaire, avec des performances intrinsèques extrêmement prometteuses. Ces algorithmes permettent-ils, en pratique, de concilier meilleure précision et performance pour les architectures multicore x86 ou hybride multicore-GPU ?
Il s'agira d'abord de dégager d'un état de l'art les BLAS de références pour les architectures visées et de définir un ensemble de benchmarks d'utilisation de ces BLAS précises. Le corps du stage consistera à développer les versions précises de ces BLAS (Round-to-Nearest BLAS) et étudier comment profiter au mieux des architectures visées selon les différents algorithmes de sommation précise. La reproductibilité des évaluations est une contrainte forte de ce travail qu'il conviendra de garantir a priori.
Les développements seront réalisés en C. Les expérimentations sur architecture hybride profiteront des moyens de calcul HPC.
URL sujet détaillé : http://perso.univ-perp.fr/langlois/index.php/fr/research-internship/12-rtn-hp-blas
Remarques : DALI peut accompagner le stagiaire dans sa recherche d'hébergement sur Perpignan (résidences universitaires, appart-hôtel) et ses environs.
|
|
|
|
|
|
SM207-94 Cryptanalyse AES
|
|
|
Description
|
|
Pendant plus d'une dizaine d'année, aucune attaque n'a été rapportée contre l'AES et depuis 3 ans, de nouvelles attaques utilisant soient un modèle très fort (related-key model) ou des variantes d'attaque par le milieu sont apparues. Ces dernières attaques permettent d'attaquer tous les tours de l'AES utilisant 128 bits de clé et ont été publiées à la conférence Asiacrypt 2011.
L'inconvénient principal des dernières attaques est qu'elles demandent une quantité de données et de temps tellement grande que personne ne peut les mettre en oeuvre. Par conséquent, il existe dans la littérature, de nombreuses attaques dont personne ne sait si elles fonctionnent réellement ou non. Un objectif du stage est de bien comprendre comment fonctionnent ces attaques contre AES et de proposer une méthode pour vérifier si les principes de l'attaque fonctionnent en pratique.
URL sujet détaillé : http://www.di.ens.fr/~fouque/stage-aes.pdf
Remarques : Possibilité d'encadrement de thèse
|
|
|
|
|
|
SM207-95 Reconstruction de graphe par un agent mobile disposant d'une vue locale
|
|
|
Description
|
|
Dans ce stage, on s'intéresse au problème de la cartographie par un agent mobile.On considère un agent mobile (qui représente un robot ou un agent logiciel) qui se déplace dans un environnement modélisé par un graphe. L'agent peut se déplacer d'un sommet à l'autre le long des arêtes du graphe et doit reconstruire une carte du graphe sous-jacent. On suppose que lorsque l'agent est sur un sommet v, il peut observer le graphe induit par les voisins de v.
On souhaite caractériser les graphes dans lesquels le problème peut être résolu lorsque le graphe est anonyme: les sommets n'ont pas d'identifiants et l'agent ne peut pas forcément distinguer deux sommets qui ont des voisinages isomorphes. Afin de caractériser ces graphes, on souhaite étudier le complexe de cliques du graphes.
On souhaite également obtenir des algorithmes efficaces pour résoudre le problème.
URL sujet détaillé : http://www.lif.univ-mrs.fr/~jchalopi/sujets/sujet-M2-chalopin.pdf
Remarques :
|
|
|
|
|
|
SM207-96 Frontière entre décidabilité et indécidabilité pour la finitude des groupes d'automates.
|
|
|
Description
|
|
Un automate avec une bande d'entrée et une bande de sortie peut être vu
comme une machine transformant un mot d'entrée en un mot de sortie. En
faisant varier l'état d'entrée de l'automate, on obtient un ensemble
d'applications sur les mots, et on peut s'intéresser au semi-groupe engendré par ces applications, voir au groupe sous certaines conditions.
Pierre Gillibert vient de montrer que le problème de finitude des semi-groupes d'automate est indécidable dans le cas général. Par ailleurs un résultat très récent montre la décidabilité de ce problème pour les groupes d'automates engendrés par des automates biréversibles (ayant une structure particulière) sur un alphabet à deux lettres.
Le but de ce stage est de déterminer plus précisément la frontière entre décidabilité et indécidabilité pour le problème de la finitude.
URL sujet détaillé : http://www.liafa.univ-paris-diderot.fr/~klimann/Stages/stage2012_2013.pdf
Remarques : Stage indemnisé selon dispositions réglementaires.
Possibilité de poursuite en thèse, financée par l'ANR JCJC MealyM.
Le stage a lieu au sein d'un groupe actif sur le sujet composé de 3 chercheurs ou enseignants-chercheurs permanents et un post-doc.
|
|
|
|
|
|
SM207-97 Study and comparison of different roughness measures on surfaces
|
|
|
Description
|
|
Context: Nowadays, 3D objects and scenes find their way into more and more applications and are most often represented by surface models. Various roughness measures have been defined on these surfaces, for a range of applications in particular contexts like fractal geometry, watermarking, visual quality assessment and control in industry, ... Roughness is a complex and important concept, which makes use of multiresolution and differential geometry, to study the surface behavior in the vicinity of a point. It refers to non integer dimensions and can be characterized with wavelet coefficients or differential notions like H=F6lder coefficients.
Our objective is to examine the different measures defined in the literature, in order to:
1. Improve the progressive compression of these surfaces. In this context a recent project (conducted in collaboration with the LE2I, LSIIT and I3S labs - in Dijon, Strasbourg and Sophia-Antipolis) has led to a characterization of three types of surfaces, relative to their frequency components: the smooth parts, the sharp features (notion of saliency) and the roughness parts ;
2. Control the roughness during the modelisation of complex surfaces (geometric modeling). This research field is currently explored in an ANR project, in collaboration with the LE2I, LIRIS and LORIA labs (in Dijon, Lyon and Nancy).
In this context, the goal of the thesis is to:
1. make an inventory of the different roughness characterization methods in the literature, and their applications ;
2. implement the methods that best suit to both applications mentioned above ;
3. compute the measures on =93textured=94 surfaces (with rough parts and/or sharp features): a supplied database can be used and completed ;
4. make statistical comparisons of the roughness maps obtained with the studied techniques and measure quantitatively the degree of linear correlation/similarity between them.
Software needs: Matlab or C++ programming, CGAL (Computational Geometry Algorithms Library), OpenGL, Linux or Windows
URL sujet détaillé :
:
Remarques : Co-encadrement avec Christian Gentil (Maître de Conférence au Le2i) - cgentil-bourgogne.fr
http://danae.u-bourgogne.fr/Equipe/Pages/gentil/
|
|
|
|
|
|
SM207-98 Axiomatisation de l'équivalence d'un calcul de processus
|
|
|
Description
|
|
Le calcul de processus d'ordre supérieur HOcore [1] a la particularité d'être Turing puissant tout en ayant une équivalence qui est décidable. Cette équivalence a été axiomatisée et correspond, à une règle prêt, à l'équivalence structurelle. En d'autre termes, dans ce calcul il n'existe (presque) qu'une seule manière d'exprimer un comportement donné.
Le stage proposé porte sur une étude formelle de cette axiomatisation, basée sur l'assistant de preuve Coq [2], et sur la conception d'un calcul dont l'équivalence coïnciderait avec l'équivalence structurelle. Un tel calcul permettrait de proposer une nouvelle alternative pour spécifier des comportements parallèles.
[1] Ivan Lanese, Jorge A Pérez, Davide Sangiorgi, and Alan Schmitt. On the Expressiveness and Decidability of Higher-Order Process Calculi. Information and Computation, 209(2):198-226
[2] http://coq.inria.fr/
URL sujet détaillé :
:
Remarques : Le stage pourra être rémunéré.
|
|
|
|
|
|
SM207-99 Tableaux et raisonnement arithmétique dans le compilateur Mezzo
|
|
|
Description
|
|
Tableaux et raisonnement arithmétique dans le compilateur Mezzo
Mezzo est un langage de programmation conçu par Jonathan Protzenko et moi-même
[1]. Il s'apparente au langage OCaml, mais propose un système de types et de
"permissions" plus puissant, qui permet d'éviter certains des dangers associés
à la concurrence et au partage accidentel de structures modifiables.
Le sujet du stage consiste, en bref, à étendre le langage Mezzo et son système
de types pour leur ajouter une notion de "tableau", ou zone de mémoire
homogène de longueur statiquement inconnue. On souhaite que le système de
types soit suffisamment puissant d'une part pour garantir que les accès aux
tableaux respectent bien les bornes, d'autre part pour permettre à un tableau
d'être découpé par la pensée en plusieurs segments qui pourront être manipulés
indépendamment (par exemple, par plusieurs threads distincts). Pour atteindre
ces objectifs, il est nécessaire que le programmeur puisse écrire au sein des
types des formules arithmétiques (par exemple, "i < j", ou "i < length(a)")
dont le compilateur vérifiera la validité, en s'appuyant sur un solveur SMT
externe.
Il existe déjà des langages de programmation qui permettent l'écriture de
formules logiques au sein des programmes, et qui en vérifient la validité en
s'appuyant sur un solveur externe [2, 3]. On pourra s'inspirer de ces systèmes
ou même (pourquoi pas) s'appuyer directement sur eux, en traduisant Mezzo vers
l'un de ces langages.
Le stage se déroulera à l'INRIA, sur le site de Rocquencourt, sous la
direction de François Pottier, de février ou mars à juillet 2013.
Une version plus détaillée du sujet de stage sera bientôt (12/11/2012) en
ligne à l'adresse http://gallium.inria.fr/~fpottier/stages/sujet2013-m2.pdf
[1] François Pottier et Jonathan Protzenko.
Programming with permissions in Mezzo.
Soumis pour publication, octobre 2012.
http://gallium.inria.fr/~fpottier/publis/pottier-protzenko-mezzo.pdf
[2] Nikhil Swamy, et al.
F*.
http://research.microsoft.com/en-us/projects/fstar/
[3] Jean-Christophe Filliâtre, et al.
Why3.
http://why3.lri.fr/
URL sujet détaillé : http://gallium.inria.fr/~fpottier/stages/sujet2013-m2.pdf
Remarques :
|
|
|
|
|
|
SM207-100 Autour de la combinatoire des cycles universels
|
|
|
Description
|
|
Un cycle universel pour un ensemble E de mots de taille n sur un alphabet A est
=96 un mot cyclique sur A
=96 dont les sous-mots de taille n sont 2 à 2 distincts
=96 tel que tout mot de E est un sous-mot du cycle.
Ainsi les mots 00011101 et 01000111 sont des cycles universels pour l'ensemble des
mots binaires de taille 3. La notion de cycle universel est une généralisation
de celle de cycles de De Bruijn, ces derniers étant les cycles universels dans
le cadre des mots binaires.
Les cycles universels sont utilisés de longue date : codes de Baudot, robotique, cryptographie, neurosciences (IRM fonctionnel) et bioinformatique (séquençage par hybridation).
Le travail demandé consistera, dans un premier temps, à rédiger un état de l'art sur les cycles universels. Par la suite, on étudiera des conjectures sur le plan espérimental et si possible du point de vue théorique.
Compétences requises : bases en combinatoire (graphes, combinatoire des mots, permutations), programmation (C, C++, Java ou autre).
URL sujet détaillé : http://le2i.cnrs.fr/Celine-Moreira-Dos-Santos,149
Remarques : Co-encadrement avec Jean-Luc Baril
Financement du stage prévu
Thèse possible à partir de septembre 2013
|
|
|
|
|
|
SM207-101 Bisimulations pour le calcul de réécriture
|
|
|
Description
|
|
Le rho-calcul [1] étend le lambda-calcul avec des notions issues de la réécriture ; en particulier, les motifs sont des éléments de premier ordre et peuvent être manipulés par les termes. Ce calcul a pour but de donner une base formelle notamment aux langages basés sur les règles de récriture tels que Tom [2]. Le but de ce stage est d'étudier la théorie comportementale du rho-calcul, c'est-à-dire de prouver formellement que deux termes du langage ont le même comportement : cela passe par la définition de relations d'équivalences sur les termes (appelées bisimulations), et l'étude de leurs propriétés. Plus précisemment, nous souhaitons adapter au rho-calcul les bisimulations déjà définies pour le lambda-calcul. Nous espérons ainsi prouver l'équivalence de motifs ou de stratégies dans le rho-calcul, voire de programmes Tom.
[1] rho.loria.fr
[2] tom.loria.fr
URL sujet détaillé :
:
Remarques : Stage co-encadré avec Horatiu Cirstea
|
|
|
|
|
|
SM207-102 VASS Simulations
|
|
|
Description
|
|
Vector addition systems with states (VASS) are simple counter systems commonly employed to model concurrent, distributed systems. They are also a highly useful formalism of restricted computing capabilities, and are often employed as an intermediate step in complexity proofs. The two problems of testing whether a VASS simulates a finite-state system, or is simulated by one, are both decidable (Jancar and Moller, 1995). These algorithms have been extended to operate in a generic way on well-structured transition systems (Abdulla et al., 2000), and we can provide Ackermannian upper bounds on their complexities. On the other hand, the best known lower bounds to date are due to Lasota (2009), who proved both problems to be ExpSpace-hard, already for a very restricted class of VASS of communication-free systems.
The objective is to find the exact complexity (lower and upper bounds) of the VASS simulation problems. This is a problem that has remained open for a while, thus any progress towards matching lower and upper bounds would already be a significant contribution.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/m2-13-sys2
Remarques :
|
|
|
|
|
|
SM207-103 Reachability in Lossy VASS
|
|
|
Description
|
|
Vector addition systems with states (VASS) are simple counter systems commonly employed to model concurrent, distributed systems. They are also a
highly useful formalism of restricted computing capabilities, and are often employed as an intermediate step in complexity proofs.
A lossy VASS can see its counter values decrease nondeterministically. Their model-checking problems have been thoroughly investigated from the decidability viewpoint (Bouajjani and Mayr, 1999), but little is known about their complexity. In particular, we only know that the reachability problem, i.e. whether a particular configuration of control state and counter values can be reached by the system, is in ExpSpace by a reduction to VASS coverability (Rackoff 1978).
A related formalism is relevance logic (Dunn and Restall, 2002), a substructural logic that attempts to capture the =93natural=94 semantics of entailment, rather than the logical one. Its
implicative fragment R→ is known to be decidable, but its complexity is an open problem. For the related conjunctive implicative fragment R∧,→ , the problem is known to be Ackermannian-complete (Urquhart, 1999), the lower bound stemming from
the complexity of reachability in lossy counter systems.
The main objective is to find the exact complexity (lower and upper bound) of the reachability problem in lossy VASS. The internship should focus on this first point, and attack the following problems if time allows:
- Investigate the relationship between lossy VASS and R→ .
- Study the complexity of provability in R→ .
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/m2-13-sys1
Remarques :
|
|
|
|
|
|
SM207-104 Certification de l'opérateur eval de JavaScript
|
|
|
Description
|
|
JavaScript est un langage de plus en plus utilisé, non seulement pour enrichir les contenus du web, mais également en tant que cible de compilation ou pour le développement d'interfaces comme dans la liseuse électronique Kindle Touch. Le projet JSCert (http://jscert.org) a pour objectif de formaliser en Coq la sémantique de JavaScript afin de prouver de manière certifiée des analyses de programme. Dans ce cadre, nous avons développé un interpréteur de JavaScript qui a été prouvé correct vis-à-vis de la sémantique formelle.
Une des spécificités de JavaScript est la présence d'un opérateur d'évaluation qui exécute le code donné sous forme d'une chaîne de caractères. Une implémentation certifiée de cet opérateur doit donc comporter un parseur lui-même certifié. Un premier objectif du stage est la conception d'un tel parseur certifié. Pour ce faire, l'étudiant pourra s'appuyer sur l'approche de Jourdan, Pottier et Leroy [1]. Tout d'abord, il sera nécessaire d'exprimer de manière formelle la syntaxe du langage en se basant sur la spécification [2]. Il faudra ensuite adapter la syntaxe pour que la méthode proposée dans [1] s'applique. Enfin, un parseur pourra être développé et l'automate extrait pourra être certifié dans l'assistant de preuve Coq. Un deuxième objectif du stage est de correctement modéliser l'interaction de la fonction eval avec le reste du programme JavaScript, qui peut être très complexe [3]. Enfin, des analyses pourront être développées pour donner des garanties sur l'exécution de code par eval.
[1] Validating LR(1) Parsers, Jacques-Henri Jourdan, François Pottier et Xavier Leroy, ESOP 2012
[2] ECMAScript Language Specification, Standard ECMA-262
[3] http://brownplt.github.com/2012/10/21/js-eval.html
URL sujet détaillé :
:
Remarques : Le stage pourra être rémunéré.
|
|
|
|
|
|
SM207-105 Reconstruction d'organes pour la réalité augmentée
|
|
|
Description
|
|
L'équipe ISIT/ALCOV oeuvre au développement d'un outil de réalité augmentée pour la coelioscopie (une technique d'intervention où le chirurgien opère avec pour seule vue une vidéo endoscopique). Le projet de l'équipe se décompose en deux axes :
1) extraction et traitement des informations présentes dans les examens préopératoires (IRM+échographie)
2) insertion des données extraites dans la vidéo de l'opération.
Le sujet de stage porte sur l'extraction de la géométrie des tissus et organes à partir des images de l'IRM. Le stagiaire participera aux recherches sur deux thèmes complémentaires :
- la segmentation semi-automatique (quelques coupes segmentées par un expert permettent d'initialiser des algorithmes d'apprentissages)
- la reconstruction 3D d'un maillage des tissus et organes à partir des pixels dans différentes coupes et directions.
Les techniques utilisées tiennent aussi bien de la théorie de l'apprentissage automatique que de la géométrie algorithmique (reconstruction de surfaces).
URL sujet détaillé : http://www.676-lelivre.com/telechargements/sujet_stage_ENS-Y_Gerard.pdf
Remarques : Co-encadrement:
Yan Gerard pour la partie mathématique du projet
Jean-Marie Favreau pour la partie informatique
PS. J'ai posé le sujet sur un site perso, notre serveur ayant subi des dommages dernièrement (site web hors-ligne en ce moment même)
|
|
|
|
|
|
SM207-106 Optimisation du positionnement de lignes caractéristiques sur les maillages surfaciques - Application à la détection d'objets géologiques
|
|
|
Description
|
|
Une problématique clé en modélisation géométrique concerne le traitement de maillages (mesh processing), notamment l'extraction d'information au sein de ces entités dites " semi-discrètes ". Dans ce contexte, des travaux récents ont été effectués dans le but de détecter automatiquement des lignes caractéristiques (lignes de crêtes et de ravins) d'une surface triangulée, dans un contexte géologique. Des résultats intéressants ont été obtenus en développant une approche originale qui prend le contre-pied des méthodes existantes. Elle ne prend en compte que la courbure (estimateur de 2ème ordre) sans en étudier ses variations, dans le but de marquer des zones d'intérêt, et combine des techniques de morphologie mathématique pour extraire un squelette et assurer la connectivité des lignes.
Toutefois, le placement des lignes obtenues n'est pas entièrement satisfaisant : l'approche proposée mettait en premier lieu l'accent sur la connectivité des résultats, la position des lignes étant un problème jusqu'alors considéré comme secondaire. L'objectif du stage est d'améliorer le placement des lignes obtenues en sortie de l'algorithme d'extraction existant. Pour repositionner les lignes, il est envisagé de développer une technique visant à optimiser la position des sommets des lignes extraites le long du maillage. Plusieurs critères d'optimisation sont envisageables (extrema de courbures principales, etc...) et devront être testés. Une phase de validation, de quantification du gain obtenu (d'un point de vue géométrique) et de comparaison avec les approches existantes constituera la fin de la période de stage.
URL sujet détaillé : http://www.dil.univ-mrs.fr/~mari/pub/sujet_vogp.pdf
Remarques : Co-encadrement : Sophie VISEUR (CEREGE)
|
|
|
|
|
|
SM207-107 MISE EN OEUVRE EFFICACE D'ALGORITHMES D'INONDATION SUR DES GRANDES IMAGES A NIVEAUX DE GRIS
|
|
|
Description
|
|
Une image à niveaux de gris peut être considérée comme un relief topographique, lorsqu'on attribue à chaque point de l'image une altitude proportionnelle à son intensité de gris. Cette représentation reste valable quel que soit le nombre de dimensions spatiales de l'image ou encore lorsque l'information d'altitude est portée par les poids attribués aux nóuds d'un graphe (éventuellement valué).
Une inondation d'un relief produit un certain nombre de lacs de profondeur quelconque. Un tel relief image représente une nouvelle image à niveaux de gris, plus simple avec moins de vallées que le relief initial. Et bien évidemment, la surface de chaque lac est plate.
L'opération duale de l'inondation consiste à araser les pics. On l'obtient en inondant le négatif d'une image avant de reprendre le négatif du résultat; on arase ainsi les pics. On peut éviter cette double négation et construire directement les opérateurs d'arasement. Ces derniers se déduisent très simplement des algorithmes d'inondation et sont de même complexité. Nous ne nous intéresserons donc ici qu'aux algorithmes d'inondation.
Les deux opérateurs d'inondation et d'arasement sont les ingrédients de base de beaucoup d'opérateurs de filtrage et de segmentation. De nombreuses inondations sont possibles pour un relief donné ; cependant il en existe une seule si on considère la plus haute inondation possible d'une fonction f sous la contrainte d'une fonction plafond g. La fonction g est une fonction quelconque, supérieure ou égale en tout point à la fonction f (comme un seuil d'altitude non nécessairement constant).
L'opérateur d'inondation maximale prend les images f et g en entrée et produit l'image de l'inondation en sortie, laquelle est une image à niveau de gris égale à l'altitude de l'inondation en tout point inondé et au relief f partout ailleurs.
Les algorithmes classiques sont de deux types: les premiers construisent le résultat par balayages itératifs de l'image, tandis que les deuxièmes contrôlent l'inondation au moyen d'une file d'attente hiérarchique. Ces algorithmes sont très lents sur des très grandes images (2D ou 3D), l'objet de stage est donc de les accélérer. On explorera plusieurs voies :
- Si on a recours à plusieurs cóurs ou processeurs, comment faut-il leur distribuer le travail de la manière la plus efficace ?
- Etudier le recours à des représentations locales du relief sous forme de flèches entre chaque point et ses voisins plus hauts ou plus bas afin de limiter le nombre d'accès à la mémoire.
- Réaliser des mises en óuvre sur processeurs vectoriels ou graphiques.
Contacts: Fernand Meyer (fernand.meyer-paristech.fr ) et Claude Tadonki (claude.tadonki-paristech.fr)
URL sujet détaillé :
:
Remarques : Encadrement conjoint:
Fernand Meyer (fernand.meyer-paristech.fr ) Claude Tadonki (claude.tadonki-paristech.fr)
|
|
|
|
|
|
SM207-108 MISE EN OEUVRE EFFICACE D'UN SYSTEME DE LOCALISATION DE TEXTE ENFOUI DANS DES IMAGES ORDINAIRES
|
|
|
Description
|
|
Les OCR (Optical Character Recognition) commerciaux sont de plus en plus performants mais leur utilisation est encore restreinte aux documents numérisés ou aux images prises dans des conditions d'acquisition maîtrisées (support plat, sans effet de perspective, le document occupant la presque totalité de l'image,..). Ils ne sont pas capables de gérer la diversité de styles, les déformations liées à la perspective ou la complexité de l'environnement. La localisation du texte enfoui est une étape nécessaire pour étendre les conditions d'utilisation des OCR existants.
Le CMM (Centre de Morphologie Mathématique) de l'Ecole des Mines de Paris a développé un système de localisation de texte enfoui pour des images tout venant. Ce système a remporté la première place dans la catégorie " localisation de texte " lors de la campagne d'évaluation d'algorithmes de traitement d'images ImagEval. Aucune contrainte temps réel n'était considérée à cette occasion. Aujourd'hui nous envisageons de porter ces algorithmes sur des dispositifs portables, type smartphone. Pour cela, un travail important de simplification et d'optimisation des algorithmes est nécessaire. Il s'agit de trouver un compromis qualité/performance satisfaisant. En effet, la puissance traitement des systèmes mobiles est modérée, de même que l'approvisionnement en énergie (généralement de modestes batteries). A partir du système mobile, on devrait donc être capable d'acquérir une image avec ses contraintes (résolution et environnement) et d'en extraire les informations textuelles dans un délai acceptable à l'échelle de l'utilisateur. Le texte deviendrait accessible aux personnes malvoyantes ou illettrées (ou ne parlant pas la langue du pays où elles se trouvent) en combinant ce système soit à un module de restitution orale ou à un module de traduction, respectivement. On peut bien sûr imaginer un télétraitement de cette phase dans une approche du type Cloud Computing, mais nous ne l'aborderons pas dans ce stage.
Le candidat retenu pour ce stage aura pour tâche principale d'accélérer un module critique de l'application développée par le CMM, de manière à répondre à l'exigence du compromis qualité/performance mentionné précédemment. Le travail se fera sur des processeurs multi-cóurs standards, très probablement en C. Toutefois, si le candidat a des compétences dans la programmation des systèmes mobiles et si le temps le permet, il pourra étendre sa contribution dans ce contexte-là.
URL sujet détaillé :
:
Remarques : Encadrement conjoint:
Beatriz Marcotegui (beatriz.marcotegui-paristech.fr)
Claude Tadonki (claude.tadonki-paristech.fr)
|
|
|
|
|
|
SM207-109 Retro-engineering of auto-modifying code by static analysis
|
|
|
Description
|
|
Our numeric society heavily depends on computer systems. Their security is challenged on a daily basis by malware e.g., the sophisticated malware Stuxnet is a striking example of the vulnerability of computer systems. Once detected, the eradication of a malware requires a precise understanding of its modus operandi. Retro-engineering a malware is a complex and mostly manual task requiring a high level of expertise. The reason is that compared to ordinary software, malware implement a multitude of counter-measures: obfuscation, cryptography, anti-debugging, self-modification...
Static analysis by abstract interpretation [1] is a methodology for proving automatically safety and security properties of programs. Abstract interpretation is formal method establishing a correctness theorem with respect to the semantics of programs. Abstract interpretation has been successfully applied to the analysis of source code. The analysis of binary code has its own difficulties [2] and the analysis of malware has its own challenges.
The ANR BINSEC project (starting Jan. 2013) aims at improving the state-of-the-art of static analyses of malware. In the BINSEC project, the Inria Celtique team will be working at adapting/designing static analyses for binary code. Self-modifying code is a feature of certain malware that is known to be a show-stopper for static analysis. The originality is that analysing self-modifying code requires abstract domains capable of representing sets of programs.
The internship is proposed in the context of the BINSEC project and is a first step toward the challenge of precisely analysing self-modifying binary code. The work will first consist in providing the semantics ground for self-modifying code by extending the model of Dynamic Bitvector Automata [3]. Based on this semantics, the work will consist in extending a previously proposed static analysis for auto-modifying code [4]. The analysis will be prototyped in OCaml.
[1] Patrick Cousot & Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL77, pages 238=97252, Los Angeles, California, 1977. ACM Press, New York, NY, USA.
[2] Balakrishnan, G., Reps, T., Melski, D., and Teitelbaum, T., WYSINWYX: What You See Is Not What You eXecute. In Verified Software: Theories, Tools, Experiments, Springer-Verlag, 2007.
[3] S. Bardin, P. Herrmann, J. Leroux, O. Ly, R. Tabary and A. Vincent. The BINCOA Framework for Binary Code Analysis] CAV 2011.
[4] S. Bardin, P. Herrmann and F. Védrine. Refinement-based CFG Reconstruction from Unstructured Programs In VMCAI 2011.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-110 Noeuds et Matroïdes Orientés
|
|
|
Description
|
|
Ce projet a pour objectif d'étudier les noeuds en utilisant la structure de matroïdes orientés pour mieux comprendre leurs propriétés algébriques et géométriques.
L'étudiant commencera par une étude de la littérature sur les noeuds (diagrammes, code de Gauss, polynômes de Hoffman, de Jones, etc.) et sur les matroïdes orientés (lien avec la convexité).
Le stagiaire étudiera analytiquement et numériquement certains aspects algébriques et géométriques de noeuds, puis il/elle fera une étude numérique ainsi qu'une modélisation en 3D de certains modèles.
L'étudiant doit avoir un forte connaissance d'une langue programmation (C, C++ ou Python) et s'intéresser à la théorie des noeuds et à la combinatoire.
URL sujet détaillé :
:
Remarques : Possibilité de rémunération
|
|
|
|
|
|
SM207-111 Détection Automatique de Cratères sur les Objets Célestes
|
|
|
Description
|
|
Le but du stage est le développement d'une méthode automatique de détection de cratères à partir d'un maillage triangulaire, préliminaire indispensable à la mesure de leurs caractéristiques. La méthode sera appliquée aux astéroïdes Eros, Vesta et Lutetia pour lesquels nous disposons des modèles 3D. Pour ce faire, une piste envisagée consistera à extraire l'ensemble des lignes caractéristiques (i.e. les lignes de ravins et les lignes de crêtes) des objets triangulés, puis d'effectuer un filtrage pour ne conserver que les cycles de sommets, caractérisant alors les cratères. De plus, une méthode de restauration devra être élaborée lorsque certains cycles ne seront pas totalement fermés. L'originalité de cette approche réside dans le traitement direct d'acquisitions 3D, contrairement aux méthodes traditionnelle qui reposent sur une analyse des images 2D pour détecter les cratères. Une étude des caractéristiques propres aux cratères (de type taille, "rondeur", profondeur) pourra compléter la méthode de détection automatique développée.
URL sujet détaillé : http://www.dil.univ-mrs.fr/~mari/pub/sujet_impact3D.pdf
Remarques : Co-encadrement : Laurent JORDA (LAM, Laboratoire d'Astrophysique de Marseille)
|
|
|
|
|
|
SM207-112 Lattice Reduction Simulation
|
|
|
Description
|
|
Lattice reduction has been growing as one of the main tool of modern cryptanalysis. Lattice reduction allows to cryptanalyze a wide range of cryptosytems, including the classic RSA with Coppersmith method, NTRU, the GGH type schemes, the hash function SWIFFT and SWIFTTX based on Q-ary lattice, the Learning With Error based cryptosystems and all the new type of fully homomorphic schemes (from ideal lattice to Approximate GCD based cryptosystem). Hence, the importance of lattice reduction is undoubtful.
Lattice reduction is composed by a family of algorithms: starting from the historical LLL a polynomial algorithm, up to HKZ, which is an exponential algorithm. This family includes BKZ, pruning method, deep insertion variant, etc. Those algorithms are provided with an upper bounded running time and an approximation factor. Algorithms use more time, return result with lower approximation factors. The smaller the approximation factor is, the better the result will be. In cryptanalysis, it is often not required to acquire the best result. A good result will often break the cryptosystem. However, if an upper bound is provided, to date there is no answer to the main question: Whatever lattice algorithm we are using, what is the minimum time to obtain a given quality (i.e., the approximation factor)? The underlying question as how to fix the parameters, that will enable the cryptosystem to be secure: if you know your best lattice reduction will take 2^100 operation, you know your cryptosystem is secure.
To solve this problem, cryptanalysts do an overkill technique by using extremely huge parameters under which they are sure that the resulting cryptosystems will be secure, and therefore compromise the efficiency of such cryptosytems. Hence, it is clear that the adoption of the new techniques in practical will not be practical. This has been demonstrated by the breakthrough result of fully homomorphic encryption, which is supposedly very useful in securing the cloud technology, but to date, there is no adoption of this technology yet, due to its impracticality.
This project intend to study all existing lattice reduction algorithms by performing simulation on all different types of lattice, which can be encountered by cryptanalyst. The result provide the gap between theory and practice.
The outcome of this project is an implementation, i.e. a software, which for a given lattice and a given approximation factor, after a short process will provide essential information, namely: which algorithm to use, with which parameter, and an estimate of the running time. Then, it will start the corresponding algorithm with proper parameters and constant re-evaluation of estimated time.
URL sujet détaillé :
:
Remarques : A Ph.D position with scholarship may follow.
|
|
|
|
|
|
SM207-113 Homomorphic Monte Carlo based medical treatment planning
|
|
|
Description
|
|
Homomorphic encryption is a solution for enabling operations on the encrypted data. Recently, Gentry successfully provided a framework for constructing homomorphic encryption schemes and, further, he provided a concrete construction using ideal lattice. In addition, subsequent works based on his framework have been proposed recently.
The problem of developing a fully homomorphic public key encryption scheme has been a long-standing open problem in the cryptography research community. Shortly after Shamir, Rivest, and Adleman invented RSA, Rivest, Adleman, and Dertouzos questioned whether a fully homomorphic encryption scheme, which they called a privacy homomorphism, can be constructed. If such a scheme can be constructed, then essentially one can arbitrarily compute using encrypted data. Essentially, fully homomorphic encryption schemes enable one to apply homomorphic operations over an arbitrary number of given ciphertexts c1,c2,...,cn without the need to know the corresponding plaintexts m1,m2,...,mn.
This feature has potential to be useful in the cloud computing scenario, where one can upload encrypted data to the cloud and enable the cloud to process the data without the need for decryption.
This project aim to create a homomorphic version of a Monte Carlo based medical treatment planning.
URL sujet détaillé :
:
Remarques : A Ph.D position with scholarship may follow.
|
|
|
|
|
|
SM207-114 Formal Verification of Distributed Algorithms
|
|
|
Description
|
|
The context of this project is the formal verification of parallel and distributed algorithms through model-checking. The proposed work will build upon the PlusCal modeling language from the TLA+ framework. The goal is to enable the verification of algorithms under different assumption regarding the network and memory models.
For a complete presentation of the subject please see the detailed description in PDF file referenced below.
URL sujet détaillé : http://www.loria.fr/~merz/stages/pluscal-extensions.pdf
Remarques : The subject is at the intersection of the formal verification and distributed algorithms communities; it is proposed jointly with Martin Quinson of the AlGorille team.
|
|
|
|
|
|
SM207-115 Frontière entre décidabilité et indécidabilité pour la
|
|
|
Admin
|
|
| Encadrant : Stephan MERZ |
| Labo/Organisme : LORIA |
| URL :
: |
| Ville : Nancy |
|
|
|
|
Description
|
|
The context of this project is the formal verification of parallel and distributed algorithms through model-checking. The proposed work will build upon the PlusCal modeling language from the TLA+ framework. The goal is to enable the verification of algorithms under different assumption regarding the network and memory models.
For a complete presentation of the subject please see the detailed description in PDF file referenced below.
URL sujet détaillé : http://www.loria.fr/~merz/stages/pluscal-extensions.pdf
Remarques : Stage indemnisé selon dispositions réglementaires.
> Possibilité de poursuite en thèse, financée par lANR JCJC MealyM. Le
> stage a lieu au sein d'un groupe actif sur le sujet composé de 3
> chercheurs ou enseignants-chercheurs permanents et un post-doc.
> ---------------------------------------------------------------------
> Après acceptation du stage par l'ENS, votre sujet sera mis en ligne
> pour les étudiants.
> ---------------------------------------------------------------------
Le 08 Nov 2012 a 14:05:30, Laurent Lefevre a écrit :
> Le 08/11/12 14:03, Ines Klimann a écrit :
>>Bonjour,
>>
>>
>>
>>j'avais soumis il y a quelques jours une proposition de stage qui
>>n'apparaît pas sur votre page. Comme la date limite approche et que
>>celle d'un collègue ayant soumis après moi est affichée, je me suis
>>permis de resoumettre la proposition.
>>
>>Cordialement,
>>Ines Klimann.
>>
> je viens de mettre a jour
> cdt
>
> L.L.
>
> --
>
> ---
> Dr Laurent LEFEVRE, Permanent INRIA Researcher
> High Performance Networks, protocols and services
> INRIA RESO - LIP (UMR CNRS, INRIA, ENS, UCB)
> Bureau 370, Ecole Normale Superieure
> 46, allee d'Italie - 69364 LYON Cedex 07 - FRANCE
> Tel: +33 (0) 4 7272 8228 Fax: +33 (0) 4 7272 8080
> laurent.lefevre-lyon.fr http://perso.ens-lyon.fr/laurent.lefevre
> ---
>
--
nouvelle adresse électronique (l'ancienne explosera bientôt en vol):
klimann.univ-paris-diderot.fr
Ines Klimann
LIAFA, Universite Paris 7 & CNRS
01 57 27 92 33 - bureau 6A05
From llefevre.lip.ens-lyon.fr Fri Nov 9 09:25:47 2012 +0100
Return-Path:
Received: from glaive-13-mailstore.ens-lyon.fr (localhost [127.0.0.1])
by glaive-13-mailstore (Cyrus v2.4.12-Debian-2.4.12-2) with LMTPA;
Fri, 09 Nov 2012 09:25:47 +0100
X-Sieve: CMU Sieve 2.4
Received: from jabiru.ens-lyon.fr (jabiru.ens-lyon.fr [140.77.51.2])
by glaive-13-mailstore.ens-lyon.fr (Postfix) with ESMTP id 90797140CF8
for ; Fri, 9 Nov 2012 09:25:47 +0100 (CET)
Received: from localhost (localhost [127.0.0.1])
by jabiru.ens-lyon.fr (Postfix) with ESMTP id 8DF101EB173
for ; Fri, 9 Nov 2012 09:25:47 +0100 (CET)
X-Virus-Scanned: by amavisd-new-2.6.4 (20090625) (Debian) at ens-lyon.fr
X-Spam-Flag: NO
X-Spam-Level:
X-Spam-Status: No, score=0.267 tagged_above=-5 required=5
tests=[BAYES_00=-1.5, HTML_MESSAGE=0.001, HTML_MIME_NO_HTML_TAG=0.377,
MIME_HTML_ONLY=0.723, MIME_QP_LONG_LINE=0.001, SPF_SOFTFAIL=0.665]
autolearn=no
Received: from jabiru.ens-lyon.fr ([127.0.0.1])
by localhost (jabiru.ens-lyon.fr [127.0.0.1]) (amavisd-new, port 10024)
with ESMTP id 6N+jXbiVSGWe for ;
Fri, 9 Nov 2012 09:25:46 +0100 (CET)
Received: from tetras-domu-ppi.ens-lyon.fr (tetras-domu-ppi.ens-lyon.fr [140.77.167.31])
by jabiru.ens-lyon.fr (Postfix) with SMTP id 2EC561EB21E
for ; Fri, 9 Nov 2012 09:25:43 +0100 (CET)
Received: by tetras-domu-ppi.ens-lyon.fr (sSMTP sendmail emulation); Fri, 09 Nov 2012 09:25:43 +0100
X-Originating-IP: 193.49.83.102
To:
Subject: [StageM2]
X-PHP-Originating-Script: 1166:class.mailer.php
Date: Fri, 09 Nov 2012 09:25:43 +0100
From:
X-Priority: 2
X-Mailer: WAmailer/2.1
X-Env: Linux - Apache/2.2.16 (Debian) PHP/5.3.3-7+squeeze14 with Suhosin-Patch
mod_ssl/2.2.16 OpenSSL/0.9.8o
X-AntiAbuse: Sender IP - 193.49.83.102/Server Name -
MIME-Version: 1.0
Message-ID:
Content-Type: text/html; charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Status: RO
X-Status:
X-Keywords: NonJunk
X-UID: 119
Site: : laurent.lefevre-lyon.fr
A : laurent.lefevre-lyon.fr
|
|
|
|
|
|
SM207-116 Discrétisation automatique de ℝ² vers un automate cellulaire
|
|
|
Description
|
|
Les automates cellulaires sont des systèmes dynamiques à espace et temps discret. Néanmoins, depuis longtemps, les chercheurs ont l'habitude d'expliquer la dynamique par des dessins avec un espace et un temps continus, ou inversement, de partir de conception et de constructions (continues) sur ℝ2 puis de discrétiser pour avoir l'automate cellulaire voulu. Dans un sens le passage au continu est une abstraction utile pour comprendre, dans l'autre, des " détails techniques " sont souvent plus ou moins laissés à la " sagacité du lecteur ".
Depuis une dizaine d'années, une contrepartie purement continue (en espace et en temps) aux automates cellulaires, les machines à signaux a été développée. Le but de ce stage est de considérer les possibilités de discrétiser automatiquement des machines à signaux en automates cellulaires tout en préservant diverses propriétés.
Le travail en stage va de l'implantation de discrétisations (et leur étude pragmatique) à des recherches théoriques sur une logique capable d'exprimer des propriétés valables dans le monde discret et continu et voir ce que l'on peut espérer conserver.
URL sujet détaillé : http://www.univ-orleans.fr/lifo/Members/Jerome.Durand-Lose/Recherche/Sujet/2013_ENS_Lyon_M2/index.html
Remarques : Le stagiaire bénéficiera d'un portable et d'un bureau au sein du LIFO durant la durée du stage.
Le stage est rémunéré (indemnités) et pourrait déboucher sur une thèse.
|
|
|
|
|
|
SM207-117 Algorithmes certifiés d'uniformisation de triangulations surfaciques
|
|
|
Description
|
|
L'équipe GeoMod s'intéresse aux problèmes de modélisation géométrique des formes 3D à l'aide de maillages triangulaires de qualité. Dans le cadre de son projet de modélisation interactive à destination des artistes, les contraintes d'efficacité des algorithmes utilisés ont conduit l'équipe à porter un regard nouveau sur les maillages uniformes qui peuvent être rendus compatibles avec les possibilités actuelles d'édition et de visualisation de maillages de taille importante. Le but de ce stage est de s'intéresser aux problèmes théoriques posés par la génération de triangulations uniformes d'une sous-variété Riemannienne, avec des applications au cas de la triangulation des surfaces plongées dans R3.
Contexte existant :
Nous disposons d'ores et déjà d'un algorithme de génération de maillages quasi-uniformes, avec une approche temps réel pour sculpter une forme virtuelle en autorisant tout type de déformation, y compris celles entraînant un changement de genre topologique.
Objectif du stage :
L'objectif de ce stage est de s'intéresser aux questions théoriques levées par la génération de maillages dont l'uniformité soit totalement maîtrisée, d'étudier les algorithmes existants ainsi que leur preuve et de développer un nouvel algorithme efficace intégrant la dimension volumique correspondant au plongement dans l'espace ambiant, et prenant en compte la présence possible d'arêtes dites de contrainte.
URL sujet détaillé :
:
Remarques : Le stagiaire pourra être amené à interagir avec Julie Digne et avec Lucian Stanculescu. Ce stage s'adresse tout particlulièrement à des étudiants intéressés par la géométrie algorithmique ou par la théorie des graphes. Des compétences complémentaires en programmation C++ et utilisation de la STL sont les bienvenues.
|
|
|
|
|
|
SM207-118 Real-time online emulation of real applications on SimGrid with Simterpose
|
|
|
Description
|
|
The goal of this project is to design an evaluation environment for distributed applications (e.g.; P2P applications) where the instances of the real application (a standard & unmodified BitTorrent client) are executed in a virtual environment simulated by the SimGrid simulator.
Key skills required: system programming in C on Linux; deep understanding of OS principles.
URL sujet détaillé : http://webloria.loria.fr/~quinson/Research/Students/2013-master-simterpose.pdf
Remarques : Ce stage est rémunéré; il sera co-encadré par Lucas Nussbaum, de la même équipe.
|
|
|
|
|
|
SM207-119 Classification of cycles for 2D digital objects
|
|
|
Description
|
|
One of the most elementary process in topological processing of digital objects is to classify cycles (closed digital curves) inside the object from a topological point of view. This problem is intimately linked to that of transformability of cycles, that is, given two cycles inside a digital object (square-pixel based object) to determine if one can be transformed into each other. We attack this question by installing a semicontinuous analogous structure (a two-dimensional cell complex) on the digital object
and analyzing its homology behavior. We choose this two-dimensional cell complex, guaranteeing that it is topologically equivalent to the original digital object. The last task of homology analysis will be done, reinterpreting the digital object in terms of a hierarchy of directed trees installed on the 1-skeleton of the first barycentric subdivision of the associated cell complex. The sink nodes (if there is any) of those trees, called critical cells (in fact, they are the barycenters of these cells), constitute a complete set of homology generators for the cell complex and, consequently, for the digital object. Finally, we intend to specify a "classifying" function with input the set of pixels of a cycle inside a digital object and efficiently solving both problems of classification and transformability. It is also intended to do an educational computer program in which it will be possible to experiment this algorithm with 2D digital objects. All this strategy planned here is based on the homology-based technique for analyzing digital images, called "Homological Spanning Forest" [MR12].
[MR12] Homological Spanning Forest framework for 2D Image Analysis. H. Molina-Abril and P. Real. Annals of Mathematics and Artificial Intelligence (2012) 64:385-409
URL sujet détaillé :
:
Remarques : Co-encadrement : Pedro REAL (Université de Séville, Espagne)
|
|
|
|
|
|
SM207-120 State Space Reductions for Verifying Equivalences of Security Protocols
|
|
|
Description
|
|
Formal security has had considerable success, providing tools for automatically analyzing protocols and checking that they satisfy various security properties. Reachability properties, such as secrecy, have been extensively studied. More recently, there has been a growing interest for equivalence properties, which are more complex but appear to be necessary to verify things such as anonymity, vote privacy, untraceability, etc. In this context, one naturally models security protocols using specific process algebras such as the spi-calculus or the applied π-calculus. The question is then whether two processes are indistinguishable, in any environment, which is modelled by trace equivalence. Security calculi bring specific features that make this problem very hard: one has to deal with an equational theory involving cryptographic primitives, and actions which may be indistinguishable at one point in time but not in a future where the environment has acquired more information. Complex symbolic techniques have been designed that made it possible to automate equivalence of various security calculi.
So far, little attention has been paid to the combinatorial explosion caused by the interleaving of concurrent executions of protocols, which greatly hinders the scalability of current tools. This problem is far from being specific to security protocols, and has been tackled in other contexts. Besides domain specific techniques, solutions generally rely on a precise analysis of concurrent behaviors, and sometimes involve conceptual shifts such as moving from transition systems to partial order semantics. The goal of this internship will be to propose such techniques for optimizing current protocol equivalence algorithms. This will involve theoretical work to identify the appropriate concepts and techniques and extend them to the intricate case of trace equivalence for security calculi. In addition, the proposed techniques will have to be validated by case studies. We expect immediate practical outcomes in the form of enhancements of existing implementations (e.g., Datep, SPEC, Akiss).
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/?l=fr
Remarques : This internship may be funded by the ANR project VIP.
|
|
|
|
|
|
SM207-121 Tracelet Semantics of Weak Memory
|
|
|
Description
|
|
Concurrency on modern processors is commonly thought to be difficult to
understand because of "weak" semantics, where instructions are reordered and
stores are not atomic. Tony Hoare has recently advanced a form of semantics
called the "tracelet" semantics. In tracelet models program components denote
tracelets, small portions of global partially-ordered traces. This semantics is
named by analogy with separation logic, whose semantics is based on "heaplets",
or small portions of heap. The tracelet semantics has elegant mathematical
properties, and forms a model of concurrent separation logic, a recent program
logic for concurrency. And yet, because of its reliance on partial orders, the
semantics appears to be well suited to weak memory. There is the alluring, but
as yet unrealized, possibility of an elegant semantics and logic associated to
weak memory.
The purpose of this internship opportunity is to investigate the tracelet
semantics for a programming language over weak memory, in detail. It may be
that the fit of tracelets to weak memory is good, and it may be that it is not
a good fit. Finding the answer in either case would expand knowledge. This
internship will be supervised by Jade Alglave and Peter O'Hearn. Jade has
extensive experience on modelling weak memory using partial orders, and Peter
has extensive experience on logic and semantics, particularly on separation
logic.
There is a possibility that this work may lead onto a PhD position, and partial
funding for the internship itself might be available.
URL sujet détaillé :
:
Remarques : This internship will be supervised by Jade Alglave and Peter O'Hearn. There is a possibility that this work may lead onto a PhD position, and partial
funding for the internship itself might be available.
|
|
|
|
|
|
SM207-122 Links between AI and Program Verification
|
|
|
Description
|
|
Concepts from AI have recently gained traction in program verification,
including: (i) the frame problem, that of avoiding specifying the non-effects
of actions; (ii) the ramification problem, that of understanding the indirect
effects of actions; (iii) abduction, the problem of inferring explanatory
hypotheses. These ideas have been used to boost the tractability of various
program analysis tasks. However, while verification researchers have taken
basic ideas from AI, they did not borrow technical ideas. Also, as of yet,
there has been no flow of ideas back towards AI.
The purpose of this internship opportunity is to investigate the relationship
between AI and Verification formulations of these three concepts. One would
like to know if verification techniques can help with AI problems, and
conversely. At the least, one would like to know if the solutions proposed in
one community can, in principle, solve the problems of the other. This will
involve theoretical work translating problems of one field into the language of
the other, and judging the results by theorems and by examples. There is also
the potential to do work on prototype reasoning tools.
There is a possibility that this work may lead onto a PhD position, and partial
funding for the internship itself might be available.
URL sujet détaillé :
:
Remarques : This internship will be supervised by Jules Villard and Peter O'Hearn. There is a possibility that this work may lead onto a PhD position, and partial
funding for the internship itself might be available.
|
|
|
|
|
|
SM207-123 Bringing Automation to Separation Logic
|
|
|
Description
|
|
Separation logic is a formalism that enabled computer scientists to write more simple and concise proofs of correctness for computer programs dealing with dynamic memory allocation. Many of these proofs, however, have only been written in the blackboard (on papers); and early attempts to automate such proof search have faced a number of limitations. More recently, techniques from the automated reasoning community have been successfully applied on small fragments of separation logic, boosting the possibilities of practical applications. The purpose of this internship opportunity is to study the literature to gather examples of proofs that have been already done by hand, and identify possibilities where automation techniques could be generalised to deal with larger and more expressive fragments of separation logic. This will involve theoretical work, judging the results by theorems and by examples. There is also the potential to do work on prototype theorem proving tools.
URL sujet détaillé :
:
Remarques : There is a possibility that this work may lead onto a PhD position, and partial funding for the internship itself might be available.
|
|
|
|
|
|
SM207-124 Traitement des références en réalisabilité classique
|
|
|
Description
|
|
Les derniers travaux de Krivine ont fait surgir des liens inattendus entre le forcing de Cohen et la programmation impérative, basée sur la notion d'effet de bord. Le lien découvert par Krivine a été précisé depuis dans [Miquel'11], et d'autres liens entre la réalisabilité et les effets de bord ont également été proposés dans d'autres travaux. Tous ces travaux ouvrent naturellement la voie à une extension de la correspondance preuves-programmes à la programmation impérative, suivant un nouveau paradigme dans lequel l'état mémoire (côté programmation) correspond plus ou moins à une condition de forcing (côté logique).
Le but du stage est d'étudier dans ce cadre un effet de bord très simple: le déréférencement (lecture) et l'affectation (écriture) d'une ou plusieurs références pointant sur un ou plusieurs entiers. Pour cela, l'étudiant se placera dans le cadre de la réalisabilité avec états [Miquel'09], qui permet déjà de traiter le cas d'une horloge (c'est-à-dire d'une référence en lecture seule, dont la valeur indique le temps d'exécution). Il s'agira de définir une extension de la réalisabilité classique avec états permettant de parler du contenu des références au niveau de la logique, et de donner dans ce cadre une interprétation logique aux primitives de déréférencement et d'affectation. Une piste naturelle est de considérer les références comme des entiers non standard, et de les traiter avec des outils similaires à ceux qu'on trouve en analyse non standard.
Programme de travail:
- Familiarisation avec la réalisabilité classique avec états.
- Expression sous forme d'algèbre de réalisabilité.
- Définition du modèle mémoire et du langage logique permettant d'exprimer le contenu de la mémoire.
- Définition des principes de preuves induits par la présence de l'état mémoire. Preuve d'un théorème d'adéquation.
- Liens avec l'analyse non standard. Applications.
- Éventuellement: liens avec le forcing de Cohen.
URL sujet détaillé : http://perso.ens-lyon.fr/alexandre.miquel/references.pdf
Remarques :
|
|
|
|
|
|
SM207-125 Codage compact pour la propagation d'une information dans un réseau de capteurs sans fil
|
|
|
Description
|
|
Les réseaux de capteurs sans fil sont souvent utilisés pour informer des nóuds distants d'évènements environnementaux ayant été détectés. L'état du réseau (vis-à-vis de la connaissance d'un évènement donné) évolue d'une manière particulière : les états du système forment un treillis. L'objectif de ce stage consiste à étudier les propriétés de ce treillis, pour pouvoir répondre à des questions de haut niveau à partir d'une vision partielle et éventuellement erronnée de l'état du réseau. Par exemple, on peut chercher à déterminer si la vision partielle est cohérente. On peut aussi chercher à déterminer si un pourcentage donné de nóuds a été informé de l'évènement. Le travail au cours du stage consistera essentiellement à trouver une manière de coder le treillis de manière compacte afin de pouvoir répondre efficacement aux questions de haut niveau.
URL sujet détaillé : http://sancy.univ-bpclermont.fr/~guitton/recherche/sujet-treillis-wsn.pdf
Remarques : Co-encadrant : Alexandre Guitton (LIMOS)
|
|
|
|
|
|
SM207-126 Better Approximations of VASS Reachability Sets
|
|
|
Description
|
|
Model-checking counter machines, and in particular vector additions system with states (VASS) or Petri nets, is a notoriously difficult problem. These systems are central in many
modelization paradigms. This has led to the development of a number of
verification tools capable of analyzing counter machines. The analysis usually
proceeds through the computation of under-approximations or upper-approximations
of the reachability set (or both). Under-approximations are typically obtained
by an iterative fix-point computation of the reachability set, starting from the
initial configuration. Upper-approximations based on downward-closed sets are
computed by tools implementing the classical Karp & Miller algorithm. Some
techniques, for instance abstraction-refinement and learning, combine both
approximations.
Even though the reachability problem is decidable for VASS, these tools may fail
to answer reachability questions on VASS, due to diverging computations
or imprecise approximations.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/~finkel/2012-2013/M2/m2.KM.pdf
Remarques : Le sujet est co-encadré par Alain Finkel (LSV, ENS Cachan) et Jérôme Leroux (LaBRI, Bordeaux).
Une rémunération est possible.
|
|
|
|
|
|
SM207-127 Algorithmics of infinite Downward-Closed Sets for WSTS
|
|
|
Description
|
|
The theory of emph{Well Structured Transition Systems}, (WSTS) allows the automatical verification
of infinite-state systems, that can be finitely represented and tested cite{F90,finkel98b,FGL-stacs2009,FG-lmcs12}.
Objectives
item Adapt the definitions and the results about Covering Shared Trees in cite{DBLP:journals/sttt/DelzannoRB04} to DCS.
item There exist many algorithms (and implementations) to solve the coverability problem (given a state does there exist a reachable state from such that geq s0) cite{DBLP:journals/jcss/GeeraertsRB06}, and it is not completely clear which are the most interesting. Make this more clear.
item There exist also some recent algorithms (and implementations) for computing the clover cite{DBLP:conf/apn/ReynierS11,DBLP:conf/apn/ValmariH12}. By using efficient symbolic representations for DCS and UCS, propose algorithms and efficient implementations of coverability algorithms for monotone Presburger counter machines (which subsume Petri nets and monotonic extensions of Petri nets, Affine nets).
URL sujet détaillé : http://www.lsv.ens-cachan.fr/~finkel/2012-2013/M2/m2.algo-downward.pdf
Remarques : Le sujet est encadré par Alain Finkel (LSV, ENS Cachan).
Une rémunération est possible.
|
|
|
|
|
|
SM207-128 Mathematical fundations of Well Structured Systems
|
|
|
Description
|
|
Il s'agit de continuer à explorer la théorie des WSTS renouvelée dans plusieurs papiers récents (STACS'2009 et ICALP'2009 et dont les versions journal sont en train de paraître).
URL sujet détaillé :
:
Remarques : Le sujet est encadré par Alain Finkel (LSV, ENS Cachan).
Une rémunération est possible.
|
|
|
|
|
|
SM207-129 Optimisation du chiffrement homomorphe.
|
|
|
Description
|
|
A l'heure du cloud computing, de plus en plus d'entreprises préfèrent acheter des heures de calcul sur des serveurs externes, plutôt que d'acheter leurs propres serveurs. Afin de préserver la confidentialité des données, de nouveaux principes cryptographiques ont vu le jour, tels le chiffrement homomorphe. Ces systèmes permettent d'appliquer des fonctions arbitraires (ou simuler des circuits logiques) sur des données chiffrées, de sorte que le résultat soit déchiffrable rapidement.
Ces schémas ont des représentations très diverses:
* certains reposent sur la difficulté de trouver des vecteurs courts dans des réseaux euclidiens quelconques;
* d'autres reposent sur le même problème, mais dans des anneaux de polynômes modulaires (ou encore des réseaux circulants);
* certains fonctionnent sur des corps finis premiers ou des extensions de corps finis;
* enfin certains encodent tout sur des entiers, et reposent sur l'approximate GCD (étant donné n nombres proches de multiples de p, trouver p).
L'inconvénient majeur du Fully Homomorphic Encryption scheme est la taille des entités (clés ou chiffrés), qui peuvent atteindre plusieurs méga octets pour les versions heuristiques et quelques giga pour les versions prouvées. Ainsi, chaque évaluation de porte logique correspond à au moins une multiplication dans une très large structure: réseau, corps, polynôme...
Un enjeu majeur serait de rendre le schéma plus rapide, concis et/ou léger.
Parmi les pistes possible, le(a) stagiaire pourrait étudier l'arithmétique des corps finis ou des anneaux de polynômes en étudiant des représentations non conventionnelles, ou encore travailler directement sur l'algorithmique des réseaux.
Le(a) stagiaire devra avoir de bonnes connaissances en cryptographie à base de réseaux, en arithmétique et en algorithmique.
URL sujet détaillé :
:
Remarques : Co-encadrant: Nadia El Mrabet, Université Paris 8
|
|
|
|
|
|
SM207-130 Impact de la connaissance initiale pour l'algorithmique distribuée des agents mobiles
|
|
|
Description
|
|
Dans ce stage on va s'intéresser à des problèmes d'algorithmique distribuée utilisant des agents mobiles. Un agent mobile (qui peut représenter un robot ou un logiciel) est une entité pouvant se déplacer à l'intérieur d'un environnement modélisé par un graphe.
On va se concentrer sur l'information donnée au préalable à l'agent afin de compléter la tâche qu'il lui est attribuée. Cette connaissance initiale est particulièrement importante. En effet, si l'agent ne dispose pas d'informations sur le réseau, il lui est parfois impossible de compléter une tâche. Un exemple classique d'un tel problème est celui de l'exploration avec arrêt. Un agent doit visiter tous les sommets du graphe et ensuite s'arrêter. Si l'agent ne dispose d'aucune information sur le graphe, ce problème ne peut être résolu. Pour ce problème, donner au préalable à l'agent une borne sur la taille du graphe est suffisant pour résoudre le problème.
On va étudier les problèmes suivants : exploration, cartographie d'un graphe, production d'un arbre couvrant du graphe. On essaiera de faire un compromis entre la taille de l'information donnée à l'agent (mesurée en nombre de bits) et la complexité de la solution (mesurée en nombre de déplacements de l'agents).
URL sujet détaillé : http://www.lif.univ-mrs.fr/~labourel/sujet.pdf
Remarques :
|
|
|
|
|
|
SM207-131 Craig Interpolation for Advanced Display Logics
|
|
|
Description
|
|
Craig interpolation is the logical property that for any provable entailment F |- G between formulas of the logic, one can find a "middle formula" or *interpolant* I such that both F |-=02 I and I |-=02 G are provable and every variable occurring in I occurs in both F and G. Craig interpolation is intimately connected with other key logical properties like consistency, compactness and definability while, in computer science, interpolation techniques have been applied to such problems as type inference, model checking and ontology decomposition. Whether a given logic satisfies interpolation is thus of practical importance in computer science as well as theoretical importance in logic.
Recently, Brotherston and Gore gave a general method for establishing Craig interpolation in a class of logics captured by display calculi (see linked paper). Display calculi are like sequent calculi, with the extra property that one can "focus" on any part of a sequent by moving all the surrounding structure to the other side of the proof turnstile |-. (This is like rearranging an equation for a given variable in algebra.)
This project is about extending the techniques in the aforementioned paper to obtain interpolation theorems for a wider class of (generally more complicated) displayable logics. In particular, we hope that an interpolation theorem might be obtained for the well known computer science logic BI based on Brotherston's display calculus, which would solve an important open question. Of course, this means we do not know for sure that BI has the interpolation property, and so a proof might be impossible! However, even making the attempt is likely to increase our knowledge and lead to interpolation theorems for more logics than were covered in the Brotherston and Gore paper.
Candidates for this internship will need good mathematical skills; some knowledge of mathematical logic and proof theory would be particularly advantageous.
URL sujet détaillé : http://www0.cs.ucl.ac.uk/staff/J.Brotherston/TABLEAUX11/interpolation.pdf
Remarques : This internship will be supervised by James and another member of the PPLV group at UCL. There is a possibility that the internship might lead to a PhD position at PPLV, and also a possibility that the internship might be partially funded.
|
|
|
|
|
|
SM207-132 Mise en oeuvre d'attaques physiques sur les algorithmes cryptographiques de Couplage (Pairing)
|
|
|
Description
|
|
La cryptographie basée sur le Couplage ou Pairing (Pairing Based Cryptography - PBC) est un domaine récent qui permet de réaliser des schémas cryptographiques radicalement nouveaux comme le chiffrement basé sur l'identité (IBE) ou le partage de clef tripartite en un tour. Cependant, comme pour la cryptographie classique, les implémentations logicielles et matérielles de PBC peuvent être attaquées dans le but de retrouver le secret, même si l'algorithme mathématique est sûr. De telles attaques, aussi appelées attaques physiques, peuvent se répartir en deux grandes familles: les attaques par canaux cachées et les attaques par injections de fautes. Dû à la jeunesse du domaine et aux propriétés particulières de l'opération de Couplage, aucune attaque physique n'a été démontrée en pratique, même si les principes de telles attaques sur les algorithmes de Couplage ont déjà été posés dans la littérature.
Le but de ce stage sera d'étudier la faisabilité d'attaques physiques (par faute et/ou par canaux cachés) sur un algorithme de Couplage. En se basant sur les principes déjà énoncés dans la littérature, le candidat devra d'abord proposer un scénario d'attaque. Puis il devra mettre un oeuvre ledit scénario avec comme cible une implémentation logicielle (sur processeur embarqué) de Couplage, implémentation qui lui sera fournie. Suite à cette réalisation, l'analyse mathématique devra être menée afin de tenter de retrouver les données sensibles de l'algorithme de Couplage dans le but de mesurer l'efficacité de l'attaque menée.
Ce stage sera réalisé au sein du Laboratoire Systèmes et Architectures Sécurisés (LSAS), qui est une équipe mixte CEA-Leti et Ecole des Mines de Saint Etienne basée au Centre Micro-électronique de Provence (CMP) Georges Charpak à Gardanne. A travers sa plateforme collaborative MicroPackS, le Centre Micro-électronique de Provence dispose d'équipements de pointe, et du savoir-faire associé, permettant de mesurer la robustesse des composants électroniques sécurisés contre les attaques par canaux cachés (puissance de courant ou champ électron-magnétique émis) et par injection de fautes (laser, pulse électromagnétique, sur-tensions ou "glitch" en horloge...).
URL sujet détaillé : http://www.cea.fr/ressources_humaines/stages_et_formation_en_alternance/les_offres_de_stage/liste_des_stages/mise_en_uvre_d_attaques_physiques_sur_les_algor
Remarques :
|
|
|
|
|
|
SM207-133 Génération d'invariants
|
|
|
Description
|
|
Les invariants de boucle sont un outil majeur pour gérer les boucles en analyse de programmes: des techniques génériques peuvent être utilisées pour les générer indépendamment de l'analyse dans laquelle ils sont utilisés.
Pour cette raison, il existe de nombreux travaux sur les différentes façons de les inférer automatiquement. Certains utilisent des approches purement statiques, d'autres utilisent des traces d'exécution et génèrent des invariants qui sont valables dans ces traces. Ces invariants ne sont alors pas forcément valables pour toutes les exécutions.
Les objectifs principaux de ce stage sont de faire un état de l'art des techniques de génération des invariants et de leur faiblesse, en particulier à quels cas ces techniques devraient être limitées ; partant de là, on verra comment améliorer (sur les aspects précision ou correction, par exemple) ces techniques. En particulier, on étudiera comment améliorer les techniques utilisées dans l'outil JConsume qui borne l'utilisation mémoire de programmes.
URL sujet détaillé : http://lafhis.dc.uba.ar/wiki/index.php/JConsume2_Internship_Invariant_generation
Remarques : Collaboration avec l'Universidad de Buenos Aires
|
|
|
|
|
|
SM207-134 Verification of security protocols
|
|
|
Description
|
|
Context. Security protocols are short distributed programs designed to achieve various se- curity goals on data-processing networks, such as data privacy and data authenticity, even when communications between parties take place over channels controlled by an attacker. The increasing penetration of these protocols in many important applications (Internet communications, Credit Card payment, pay-per-view devices, e-voting, ...) makes designing and establishing the security of cryptographic protocols a very important research goal.
Formal methods have demonstrated their usefulness when designing and analyzing security protocols. They indeed provide rigorous frameworks and techniques that have allowed to discover new flaws.
However, most of existing techniques are dedicated to the analysis of a single protocol, without taking into account other protocols which may be used at the same time, and this is unrealistic for several reasons.
Objectives. The goal of the internship is to develop modular reasoning about security such that we can infer security guarantees for the composition of protocols from the security gua- rantees of the individual protocols.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/m2-13-vcsd.pdf
Remarques : Ce stage pourra être indemnisé.
Ce stage sera co-encadré avec Véronique Cortier (LORIA, Nancy)
|
|
|
|
|
|
SM207-135 Verification of equivalence properties in security protocols
|
|
|
Description
|
|
Context. Security protocols are distributed programs that aim at ensuring security properties, such as confidentiality, authentication or anonymity, by the means of cryptography. Such protocols are widely deployed, e.g., for electronic commerce on the Internet, in banking networks, mobile phones and more recently electronic elections. As properties need to be ensured, even if the protocol is executed over untrusted networks (such as the Internet), these protocols have shown extremely difficult to get right. Formal methods have shown very useful to detect errors and ensure their correctness.
Many results exist in literature for analyzing reachability properties, such as confidentiality and authentication. Recently, indistinguishability properties, received a lot of attention. The notion of indistinguishability is particular useful to model different flavors of anonymity, strong versions of confidentiality and specification of security properties as ideal systems. Indistinguishability is conveniently modelled by process equivalences in extended pi calculi that allow the modeling of cryptography by the means of equational theories.
Objectives of the internship. Recently, a new procedure has been proposed for verifying such equivalence properties. The tool is based on a modeling of the protocols as first order Horn clauses, techniques from rewriting theory and a dedicated resolution procedure. The aim of the internship is to extend the scope of the procedure.
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/m2-13-sdsk1.pdf
Remarques : Ce stage pourra être indemnisé.
Ce stage sera co-encadré avec Steve Kremer (LORIA, Nancy)
|
|
|
|
|
|
SM207-136 Formalizing some combinatorial attacks in security protocols
|
|
|
Description
|
|
Context. Security protocols are distributed programs that aim at ensur- ing security properties, such as confidentiality, authentication or anonymity, by the means of cryptography. Such protocols are widely deployed, e.g., for electronic commerce on the Internet, in banking networks, mobile phones and more recently electronic elections. As properties need to be ensured, even if the protocol is executed over untrusted networks (such as the In- ternet), these protocols have shown extremely difficult to get right. Formal methods have shown very useful to detect errors and ensure their correctness.
Many results exist in literature for analyzing reachability properties, such as confidentiality and authentication. These results generally rely on the assumption that cryptographic primitives work perfectly and there is es- sentially no chance of guessing any data. However, these assumptions are unrealistic in some situations. Indeed, recent protocols attempt to achieve authentication by using an out of band channel (e.g. SMS) and require comparison of strings which are short enough for humans to compare or retype them easily. This novel sort of authentication protocols is used in many daily life applications (e.g. bank transfer) and it is important to ensure their security.
Objectives of the internship. The aim of the internship is to propose formal definitions of security for this class of protocols .
URL sujet détaillé : http://www.lsv.ens-cachan.fr/Stages/Fichier/m2-13-sdsk1.pdf
Remarques : Ce stage sera co-encadré avec Steve Kremer (LORIA, Nancy)
This internship may also lead to a PhD thesis on similar topics with funding available through the ProSecure and VIP projects.
|
|
|
|
|
|
SM207-137 Formalisation effective des réels algébriques avec Coq
|
|
|
Description
|
|
L'assistant à la preuve Coq permet, outre la vérification de programmes, la formalisation de notions mathématiques. Des théorèmes de plus en plus difficiles ont ainsi pu être formellement vérifiés (d'Alembert-Gauss, quatre couleurs, et plus récemment Feit-Thompson) et des librairies réutilisables ont été développées (C-CoRN, SSReflect).
Une des particularités de Coq est qu'il permet de manipuler à la fois de telles notions mathématiques et des algorithmes qui y ont recourt, dans un formalisme homogène.
Nous nous intéressons aux nombres réels algébriques, c'est-à-dire les réels qui sont racines de polynômes à coefficients rationnels. Ces nombres ont des propriétés intéressantes : ils forment un corps que l'on peut construire, dont on peut effectivement implémenter les opérations et qui dispose d'une égalité décidable. Il s'agit de plus d'un corps réels clos archimédien.
Ces réels algébriques sont ainsi couramment utilisés en calcul formel et en mathématiques constructives. En particulier, dans la récente preuve du théorème de Feit-Thompson, ils remplacent avantageusement les réels. Ils y sont décrits de manière constructive, à partir des polynômes et des suites de Cauchy.
L'objectif du stage proposé est de passer cette description de référence des réels algébriques à une implémentation plus efficace (toujours dans Coq), proche de celles utilisées dans les logiciels de calcul formel. La correction de cette seconde implémentation sera prouvée vis-à-vis de la première, suivant une méthodologie basée sur des raffinements.
Ce sujet est varié : il met en jeu à la fois des développements formels (séries formelles, représentation de Newton des polynômes) et des problématiques de programmation fonctionnelle pour implémenter les algorithmes, notamment la somme et le produit de deux réels algébriques.
Ce stage aura lieu au sein de l'équipe MARELLE, à l'INRIA Sophia-Antipolis, qui a participé activement à la preuve du théorème de Feit-Thompson, et se déroulera dans le cadre du projet Européen ForMath dont l'objectif est de développer de nouvelles librairies de mathématiques, à la frontière entre mathématiques constructives, formalisation et calcul formel.
URL sujet détaillé : http://www-sop.inria.fr/members/Yves.Bertot/internships/algebraic_reals.pdf
Remarques : Connaissance préalable de Coq fortement recommandée.
|
|
|
|
|
|
SM207-138 Algorithmes coinductifs pour automates non standard
|
|
|
Description
|
|
Nous avons récemment proposé un algorithme pour l'équivalence de langages d'automates finis non déterministes, en s'appuyant sur des techniques traditionellement employées dans le domaine de la concurrence et des calculs de processus: les bisimulations up to.
Grâce à ces techniques, notre algorithme semble plus efficace que tous les algorithmes connus à ce jour (Hopcroft&Karp, partition refinment, antichaînes):
http://perso.ens-lyon.fr/damien.pous/hknt
Nous proposons d'étudier dans ce stage la possibilité d'étendre ce nouvel algorithme à d'autres types d'automates, très utilisés en pratique : automates de B=FCchi, automates alternants, automates d'arbres, etc...
[1] F. Bonchi and D. Pous. Checking NFA equivalence with
bisimulations up to congruence, to appear in Proc. POPL 2013.
URL sujet détaillé : http://perso.ens-lyon.fr/damien.pous/stages
Remarques : coencadrement : Filippo Bonchi et Damien Pous
|
|
|
|
|
|
SM207-139 Limites continues d'automates cellulaires
|
|
|
Description
|
|
Le motivation pour initier ce travail était de voir si l'on peut obtenir un système continu, régi par des équations aux dérivées partielles, aussi complexe que n'importe quel automate cellulaire. Un premier résultat nous a permis de trouver une classe non triviale C d'automates cellulaires pouvant admettre une limite dans un modèle continu. Le but du stage est de poursuivre cette étude, d'une part, en caractérisant quels sont les automates cellulaires qui composent la classe C pour en déduire un système différentiel chaotique voire universel afin de répondre au problème initial.
URL sujet détaillé : http://www.lacl.fr/cervelle/StageM2.pdf
Remarques :
|
|
|
|
|
|
SM207-140 Théorie algorithmique des nombres et synthèse de filtres numériques
|
|
|
Description
|
|
Un filtre numérique est un composant électronique permettant de réaliser une transformation d'un signal (audio, vidéo, réseau) en général de facon à en améliorer la qualité, ou en supprimer des composantes inutiles ; les exemples les plus classiques sont les filtres passe-bas, passe-haut, passe-bande, etc.
L'action du filtre dans le domaine fréquentiel est décrite mathématiquement par la donnée d'un polynôme (cas des filtres à reponse impulsionnelle finie) ou d'une fraction rationnelle (cas des filtres à reponse impulsionnelle infinie), sa fonction de transfert, qui résume ses propriétés. Aussi, la fonction de transfert d'un filtre passe-bas doit se rapprocher d'une fonction égale à 1 pour les basses fréquences, et nulle pour les hautes fréquences.
Diverses techniques d'approximation existent pour calculer des polynômes ou des fractions rationnelles vérifiant des contraintes en fréquence. Elles ont pour point commun de produire des polynômes ou des fractions rationnelles à coefficients réels, qui sont donc difficiles à implanter dans un composant, qui ne peut manipuler que des nombres à précision finie. Il faut donc réaliser une phase d'arrondi. L'expérience montre que les choix d'arrondi sont stratégiques, en ce sens qu'un bon choix peut permettre de diminuer significativement la difficulté d'implémentation du filtre à qualité égale.
L'objet du stage est d'étudier les stratégies d'arrondi pour ces fonctions de transfert. Le stage débutera par l'étude du cas polynomial, utilisant des techniques de programmation linéaire et de réduction des réseaux euclidiens. Dans un second temps, la/le stagiaire prendra en compte les spécificités du cas rationnel ainsi que de l'application visée (difficultés liées à la variation des pôles en fonction du choix de l'arrondi) pour étudier des stratégies d'arrondi permettant d'améliorer l'existant. Le travail théorique et algorithmique effectué aura vocation à être implanté en logiciel.
URL sujet détaillé : http://perso.ens-lyon.fr/nicolas.brisebarre/master2-2012-13-gh-nb.html
Remarques : Le stage sera co-encadré par Guillaume Hanrot (AriC, LIP, ENS Lyon).
Ce stage pourra faire l'objet d'une gratification, qui dépendra du profil de l'étudiant.
Ce sujet est susceptible de se poursuivre en une thèse.
|
|
|
|
|
|
SM207-141 Partition des graphes orientés
|
|
|
Description
|
|
Une coloration d'un graphe non-orienté est une partition des sommets
en ensembles stables (c'est-à-dire en ensembles induisant des
sous-graphes sans arêtes). L'étude de la coloration des graphes
non-orientés est un domaine déjà bien balisé, et la plupart des
problèmes encore ouverts sont reconnus comme particulièrement difficiles.
Dans ce stage on s'intéresse à un analogue de la coloration pour les
graphes dirigés, introduit en 1982 par Neumann-Lara~cite{Neu82}. Dans
ce cadre, on cherche à partitionner l'ensemble des sommets d'un graphe
dirigé en sous-graphes acycliques (c'est-à-dire sans cycles
dirigés). Cette coloration a de nombreux points communs avec la
coloration des graphes non-orientés, et il n'existe pour le moment pas
d'explication générale permettant de comprendre les similarités entre
ces types de coloration.
Nous nous intéresserons plus particulièrement aux
graphes planaires orientés. Le célèbre emph{Théorème des 4 couleurs}
dit que tout graphe planaire non-orienté peut être colorié avec 4
couleurs. Il est facile de montrer que tout graphe planaire orienté
peut être partitionné en 3 graphes
acycliques. Neumann-Lara~cite{Neu82} a conjecturé que tout graphe
planaire orienté peut être partitionné en 2 graphes acycliques. Une réponse positive à cette
question impliquerait que tout graphe planaire orienté à
contient un sous-graphe acyclique à /2. Le but du stage est
d'explorer cette version plus faible.
Elle semble liée à
une autre célèbre conjecture d'Albertson et Berman qui dit
que tout graphe planaire non-orienté à contient une forêt
(un graphe acyclique non-orienté) à /2.
URL sujet détaillé :
:
Remarques : Ce stage est co-encadré par Louis Esperet, membre
du laboratoire G-SCOP à Grenoble.
|
|
|
|
|
|
SM207-142 Renewable Energy and the Smart Grid
|
|
|
Description
|
|
There is a strong incentive today to increase the use of renewable resources of energy. While the energy derived from the wind or sun is clean and with low operational costs, its large-scale deployment will introduce higher variability, greater uncertainty and increased dynamics in the power grid.
Traditionally, the energy production was driven by the predicted demand. Allowing distributed production and highly volatile energy resources brings new challenges to the power grid. The main difficulty comes from very limited possibilities of power storage; power production and demand must be matched as close as possible at any time.
The objective of this internship is to propose a basic model for distributed energy production taking into account its volatility, and investigate the possibilities of different resources for control (responsive generators, energy storage, controlable demand).
URL sujet détaillé : http://www.di.ens.fr/~busic/stages/stageM2_energy.pdf
Remarques : Possibilité de poursuivre des travaux en thèse.
|
|
|
|
|
|
SM207-143 Génération aléatoire de structures combinatoires
|
|
|
Description
|
|
La simulation parfaite a été introduite par Propp et Wilson en 1996. Il s'agit d'un algorithme de simulation qui fournie un échantillon non-biaisé de la distribution stationnaire d'une chaîne de Markov finie.
L'objectif de ce stage est d'étudier cette technique dans le contexte de la génération aléatoire de structures combinatoires, et en particulier celles issus de la théorie des graphes. Par exemple, comment générer de manière efficace un ensemble indépendant ou encore un couplage (matching) de taille maximale. La difficulté principale consiste à trouver une chaîne de Markov qui a la distribution stationnaire souhaitée sur les objets étudiés.
Un autre objectif est d'étudier les liens entre le temps de couplage de la chaîne de Markov
et la complexité algorithmique des problèmes énumératifs.
URL sujet détaillé : http://www.di.ens.fr/~busic/stages/stageM2_simParf.pdf
Remarques : Co-encadrement avec Anne Bouillard.
Possibilité de rémunération. Possibilité de poursuivre des travaux en thèse.
|
|
|
|
|
|
SM207-144 Modélisation des relations de spécialisation et de généralisation du sens d'un mot en lambda calcul typé du second ordre
|
|
|
Description
|
|
La sémantique est le parent pauvre de la linguistique informatique, et c'est pourtant une question cruciale aussi bien pour le développement d'applications de traitement automatique des langues que pour la modélisation du processus humain de compréhension de la langue.
Nous avons proposé une modélisation de la sémantique compositionnelle en lambda calcul typé du second ordre (système F de Girard). Dans ce cadre, nous rendons compte de constructions sémantique (quantifications généralisées, pluriels) et de l'adaptation du sens d'un mot au contexte, appelée pragmatique lexicale.
Pour cette famille de phénomènes, les relations de spécialisation (voiture pour véhicule) et de généralisation (véhicule pour voiture) jouent un rôle particulier. Le but de ce stage est de définir une forme de sous typage en lambda calcul du second ordre qui corresponde à ces relations de spécialisations et de généralisation.
URL sujet détaillé : http://http
Remarques : Ce genre de questions peut naturellement s'étendre et s'approfondir en un sujet de thèse.
|
|
|
|
|
|
SM207-145 Autour d'un nouvel algorithme de résolution de systèmes d'équations linéaires modulo p
|
|
|
Description
|
|
La résolution de systèmes d'équation linéaires est un problème en apparence simple et fondamental, et pourtant il semble que tout n'ait pas été dit. Cet été, un chercheur américain, Prasad Raghavendra, a décrit un nouvel algorithme probabiliste, d'une simplicité désarmante, pour résoudre des systèmes modulo p (http://www.eecs.berkeley.edu/~prasad/linsystems.pdf).
Ce problème trouve de nombreuses application où les performances sont cruciales, notamment en cryptographie. La décomposition de grands entiers en produit de facteurs premiers nécessite notamment de résoudre de grands systèmes linéaires très creux, modulo 2.
Autant le nouvel algorithme ne semble pas pouvoir améliorer asymptotiquement les méthodes classiques, il a l'avantage de pouvoir s'adapter automatiquement au caractère creux des systèmes à traiter.
L'objectif du stage consiste à programmer l'algorithme, puis à l'étudier. Cela peut prendre de nombreuses directions. Une comparaison avec l'état de l'art est souhaitable dans tous les cas. On pourrait ensuite étudier sa parallelisation (c'est non-trivial, car l'algorithme semble inhérement séquentiel). Enfin, on pourrait par exemple essayer de l'adapter aux problèmes LPN et LWE, c'est-à-dire au cas où les équations sont "perturbées". Ceci est également intéressant du point de vue de la cryptographie.
URL sujet détaillé : http://www.lifl.fr/CALFORME/pmwiki/index.php?n=MasterI.Stage-2012-2
Remarques : Le stage est co-encadré par François Boulier (HDR), http://www.lifl.fr/~boulier/
Le stage est (modestement) rémunéré. Il peut éventuellement se poursuivre par une thèse dans l'équipe calcul formel.
|
|
|
|
|
|
SM207-146 Analyse statique de la complexité des programmes impératifs
|
|
|
Description
|
|
La complexité implicite s'intéresse à l'analyse de la complexité des programmes en élaborant des critères (systèmes de types, interprétations sémantiques) permettant de prouver qu'un programme appartient à une classe de complexité donnée. Une nouvelle analyse basée sur un système de type des langages impératifs a été proposée récemment. Cette analyse s'inspire de techniques de tiering et de non-interférence pour assurer la sécurité des programmes par analyse statique, garantissant qu'un programme impératif simple typé s'exécute en temps polynomial et/ou en espace polynomial. L'objectif de ce stage est d'implanter un programme permettant de vérifier de telles propriétés par inférence de type et d'étendre l'ensemble des programmes analysés (Fork, Threads, Objet,...).
URL sujet détaillé : http://www.loria.fr/~pechoux/stages/stageM2.pdf
Remarques : Stage co-encadré par Emmanuel Hainry (emmanuel.hainry-lyon.org)
|
|
|
|
|
|
SM207-147 Optimisation du positionnement de lignes caractéristiques sur les maillages surfaciques - Application à la détection d'objets géologiques
|
|
|
Description
|
|
Une problématique clé en modélisation géométrique concerne le traitement de maillages (mesh processing), notamment l'extraction d'information au sein de ces entités dites " semi-discrètes ". Dans ce contexte, des travaux récents ont été effectués dans le but de détecter automatiquement des lignes caractéristiques (lignes de crêtes et de ravins) d'une surface triangulée, dans un contexte géologique. Des résultats intéressants ont été obtenus en développant une approche originale qui prend le contre-pied des méthodes existantes. Elle ne prend en compte que la courbure (estimateur de 2ème ordre) sans en étudier ses variations, dans le but de marquer des zones d'intérêt, et combine des techniques de morphologie mathématique pour extraire un squelette et assurer la connectivité des lignes.
Toutefois, le placement des lignes obtenues n'est pas entièrement satisfaisant : l'approche proposée mettait en premier lieu l'accent sur la connectivité des résultats, la position des lignes étant un problème jusqu'alors considéré comme secondaire. L'objectif du stage est d'améliorer le placement des lignes obtenues en sortie de l'algorithme d'extraction existant. Pour repositionner les lignes, il est envisagé de développer une technique visant à optimiser la position des sommets des lignes extraites le long du maillage. Plusieurs critères d'optimisation sont envisageables (extrema de courbures principales, etc...) et devront être testés. Une phase de validation, de quantification du gain obtenu (d'un point de vue géométrique) et de comparaison avec les approches existantes constituera la fin de la période de stage.
URL sujet détaillé : http://www.dil.univ-mrs.fr/~mari/pub/sujet_vogp.pdf
Remarques : Co-encadrement : Sophie VISEUR (CEREGE)
|
|
|
|
|
|
SM207-148 Coalgèbres terminales d'endofoncteurs polynomiaux
|
|
|
Description
|
|
Les foncteurs polynomiaux sont une famille importante de foncteurs, très utilisée pour ses bonnes propriétés combinatoires [1].
Adamek et Porst [2] proposent une construction de la coalgèbre terminale d'endofoncteurs polynomiaux, dans le cas particulier des endofoncteurs d'ensembles.
Le sujet du stage consiste à généraliser leur résultat en utilisant les méthodes de haut niveau développées par J. Kock [1]. On considérera d'abord le cas des endofoncteurs de familles d'ensembles, puis, si le temps le permet, on explorera le cas des foncteurs polynomiaux entre catégories de préfaisceaux.
[1] J. Kock. Polynomial functors and trees. IMRS, 2011 (3).
[2] J. Adamek et H.-E. Porst. On tree coalgebras and coalgebra presentations. TCS, 2004 (311).
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-149 Préfaisceaux innocents
|
|
|
Description
|
|
Dans des travaux récents, notamment avec D. Pous [1,2,3], on développe une sémantique pour CCS, à mi-chemin entre les sémantiques de préfaisceaux [4] et les sémantiques de jeux [5]. Cette sémantique peut être vue comme une sémantique de préfaisceaux innocente, aussi bien que comme une sémantique de jeux non-déterministe.
Un travail en cours avec T. Seiller étend notre approche au pi-calcul de R. Milner.
Le sujet du stage consiste à explorer d'autres adaptations: lambda-calcul, ambients, imp, ou autre proposition faite par le stagiaire. Dans le même temps, le stagiaire contribuera au développement d'une éventuelle généralisation de l'approche.
[1] T. Hirscho et D. Pous. Innocent strategies as presheaves for CCS. In ICE '11.
[2] T. Hirscho et D. Pous. Innocent strategies as presheaves for CCS (expanded version). SACS 22(1), 2012.
[3] T. Hirscho. Full abstraction for fair testing in CCS. 2012, soumis.
[4] G. L. Cattani et G. Winskel. Presheaf models for concurrency. In CSL '96, LNCS 1258.
[5] M. Hyland. Game semantics. In Semantics and Logics of Computation. CUP, 1997.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-150 Détection Automatique de Cratères sur les Objets Célestes
|
|
|
Description
|
|
Le but du stage est le développement d'une méthode automatique de détection de cratères à partir d'un maillage triangulaire, préliminaire indispensable à la mesure de leurs caractéristiques. La méthode sera appliquée aux astéroïdes Eros, Vesta et Lutetia pour lesquels nous disposons des modèles 3D. Pour ce faire, une piste envisagée consistera à extraire l'ensemble des lignes caractéristiques (i.e. les lignes de ravins et les lignes de crêtes) des objets triangulés, puis d'effectuer un filtrage pour ne conserver que les cycles de sommets, caractérisant alors les cratères. De plus, une méthode de restauration devra être élaborée lorsque certains cycles ne seront pas totalement fermés. L'originalité de cette approche réside dans le traitement direct d'acquisitions 3D, contrairement aux méthodes traditionnelle qui reposent sur une analyse des images 2D pour détecter les cratères. Une étude des caractéristiques propres aux cratères (de type taille, "rondeur", profondeur) pourra compléter la méthode de détection automatique développée.
URL sujet détaillé : http://www.dil.univ-mrs.fr/~mari/pub/sujet_impact3D.pdf
Remarques : Co-encadrement : Laurent JORDA (LAM, Laboratoire d'Astrophysique de Marseille)
|
|
|
|
|
|
SM207-151 Déduction automatique modulo
|
|
|
Description
|
|
En déduction automatique, la tendance actuelle consiste à développer des
fondements théoriques, ainsi que des outils pratiques, qui visent à démontrer
efficacement des théorèmes qui utilisent des théories. Dans ce domaine,
certaines méthodes de déduction modernes tendent à donner des résultats très
prometteurs. En particulier, c'est le cas de la déduction modulo, qui présente
la théorie sous la forme d'un système de réécriture au lieu d'axiomes,
transformant des étapes de déduction en calculs et permettant ainsi de produire
des preuves plus courtes.
L'objectif de ce stage est d'intégrer la déduction modulo à Zenon, qui est un
outil de démonstration automatique au premier ordre basé sur la méthode des
tableaux avec égalité. Pour réaliser cette intégration, on pourra s'inspirer
d'une expérimentation récente, qui a consisté à étendre Zenon à la
superdéduction, à savoir une variante de la déduction modulo où la théorie est
présentée sous la forme de sur-règles de déduction (règles de déduction
compilées).
Afin de tester l'intégration de la déduction modulo à Zenon, un autre objectif
de ce stage est de réaliser une instanciation avec la théorie des ensembles de
la méthode B. Cette instanciation devrait permettre de vérifier automatiquement
des obligations de preuve provenant de la formalisation d'applications B. Cette
expérimentation se situe dans le cadre du projet ANR BWare
(http://bware.lri.fr/), qui a pour objectif de fournir un environnement mécanisé
permettant d'effectuer la vérification automatique d'obligations de preuve
provenant du développement d'applications industrielles utilisant la méthode B.
URL sujet détaillé : http://cedric.cnam.fr/~delahaye/stage.pdf
Remarques : Stage rémunéré et co-encadré par David Delahaye, Damien Doligez, et Olivier Hermant. Possibilité de poursuite en thèse financée.
|
|
|
|
|
|
SM207-152 Vérification formelle d'un calcul multiprécision de pi
|
|
|
Description
|
|
Pour augmenter la précision de certains calculs, il existe des bibliothèques de calcul dites ``multiprécision'', pour lesquelles chaque résultat est calculé avec une précision choisie par l'utilisateur. La correction des algorithmes repose sur une preuve papier si complexe que même des experts peuvent ne pas en être complètement sûrs. Une preuve formelle permettrait d'augmenter la confiance en de tels algorithmes puisque la vérification serait alors laissée à l'ordinateur.
L'objectif de ce stage est de développer un jeu de théorèmes qui rende possibles et aisées de telles preuves formelles en Coq. Un exemple d'application est le calcul de pi par MPFR, qui inclut à la fois des propriétés de type numérique (propagation d'erreur) et de type mathématique (convergence).
URL sujet détaillé : http://www.lri.fr/~sboldo/files/stageM2.pdf
Remarques : Co-encadrement avec Guillaume Melquiond
Rémunération possible
|
|
|
|
|
|
SM207-153 Analysing spike train statistics from real cell recordings
|
|
|
Description
|
|
Your work will focus on finding efficient approaches to extract
repeating patterns in real cell recordings. To do so, you will consider several approaches from the state of the art (e.g., Spike Pattern Association Neurons, Chronotron and STDP) and compare them on simulated data and real cell recordings. You will be part of an interdisciplinary European project entirely devoted to better understand the retina (from studying its activity and architecture, to developing new applications). You will directly collaborate with neuroscientists from our network.
URL sujet détaillé : http://www-sop.inria.fr/neuromathcomp/public/jobs-details/2012111-internship-pkornp.pdf
Remarques :
|
|
|
|
|
|
SM207-154 Counting Proof Nets
|
|
|
Description
|
|
Proof nets are graphical structures that abstract away unnecessary bureaucracy that usually comes with formal proofs, as for example, rule permutations in sequent calculus. Thus, proof nets are concise representations of formal proofs. We can therefore reduce the question
``How many proofs does a certain formula have?''
to the question
``How many proof nets do exists for this formula?''
This way, a proof theoretical question becomes a combinatoric question. The task for this internship is apply the methods of analytic combinatorics to investigate the number of proof nets of a given size.
Requirements: Basic knowledge in logic or analytic combinatorics
URL sujet détaillé : http://www.lix.polytechnique.fr/~lutz/stages/stage-countPN.pdf
Remarques :
|
|
|
|
|
|
SM207-155 Invariants of proofs in classical logic
|
|
|
Description
|
|
The questions =93What is a proof?=94 and =93When are two proofs the same?=94 are fundamental for
proof theory. But for the most prominent logic, Boolean (or classical) propositional logic, we
still have no satisfactory answers.
This is embarrassing not only for proof theory itself, but also for computer science, where
classical propositional logic plays a major role in automated reasoning and logic programming.
Also the design and verification of hardware is based on classical Boolean logic. Every area
in which proof search is employed can benefit from a better understanding of the concept of
proof in classical logic, and the famous NP-versus-coNP problem can be reduced to the question whether there is a short (i.e., polynomial size) proof for every Boolean tautology.
Usually proofs are studied as syntactic objects within some deductive system (e.g., tableaux,
sequent calculus, resolution, ...). Invariants for proofs are mathematical objects that abstract
away from the syntax, in order to be able to distinguish proofs, in the same sense as homology
groups serve as invariants to distinguish topological spaces. Examples of invariants for proofs are proof nets, logical flow graphs, combinatorial proofs, and atomic flows.
The task for this internship is to study these invariants, in particular, compare their behaviour
with respect to proof normalization, and investigate correctness criteria that allow to recover the full syntactic proof from the invariant.
The topic can be extended to a PhD thesis topic.
Requirements: Basic knowledge in logic and proof theory.
URL sujet détaillé : http://www.lix.polytechnique.fr/~lutz/stages/stage-invariants.pdf
Remarques :
|
|
|
|
|
|
SM207-156 Complexité implicite
|
|
|
Description
|
|
En complexité implicite, on cherche des critères syntaxiques sur les programmes pour assurer des bornes sur le temps de calcul (usuellement, le temps polynomial).
La méthode des Quasi-Interpétations et celle des polynômes mwp, bien que d'apparences très différentes, utilisent des techniques similaires et sont en fait très proches.
Le but du stage est de poursuivre la comparaison en essayant tout d'abord d'établir une méthode inspirée des polynômes mwp pour les systèmes de réécriture pour pouvoir aisément comparer avec les quasi-interprétations.
URL sujet détaillé : http://lipn.univ-paris13.fr/~moyen/stages_M2/sujMoyen.pdf
Remarques :
|
|
|
|
|
|
SM207-157 Plugin gcc pour calculer en espace linéaire
|
|
|
Description
|
|
La complexité implicite cherche des critères syntaxiques pour décider des propriétés sur le temps ou l'espace de calcul des programmes.
Dans ce domaine, la technique des fonctions Non Size Increasing donne un critère simple pour caractériser l'espace linéaire uniquement en comptant les allocations (malloc) et désallocations (free) de mémoire dans un programme.
L'idée du stage est d'implémenter ce critère dans un compilateur comme gcc pour obtenir des programmes dont l'utilisation de mémoire est certifiée avant l'exécution, évitant ainsi les fuites de mémoire.
Le stage comporte une partie théorique sur la compréhension de la méthode et une partie implémentation sur la modification du compilateur pour valider cette méthode.
URL sujet détaillé : http://lipn.univ-paris13.fr/~moyen/stages_M2/sujDanjean-Moyen.pdf
Remarques : Co-encadrement avec V. Danjean (Université de Grenoble) et possibilité de faire le stage soit à Grenoble, soit à Paris.
|
|
|
|
|
|
SM207-158 Mapping the Indoor Environment Using Radio Angle-of-Arrival
|
|
|
Description
|
|
Ongoing research in indoor wireless localization is showing that processing angle-of-arrival information---the physical angles at which a wireless signal arrives---from WiFi access points can achieve very fine-grained accuracy. This project will use radio angle-of-arrival
information to map geometric locations of objects and walls in the indoor environment. Using an eight-antenna experimental mobile 802.11 WiFi radio platform, we will measure the ambient radio signals in our building as they bounce off walls and other objects. Then we will apply novel search algorithms to deduce where walls are, using Markov chain Monte-Carlo and ray-tracing techniques to prune the enormous search
space.
There is a possibility that this work may lead on to PhD position in the Networks or Virtual Environments and Graphics Groups at University College London, and partial funding for the internship itself may be available.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-159 Practical Sphere Decoding for High-Throughput, Future Wireless Systems
|
|
|
Description
|
|
Spatial Multiplexing (SM) is an efficient transmission technique that can
increase the throughput of wireless communication systems when they are
equipped with multiple transmit and receive antennas (i.e., MIMO systems). In
contrast to single antenna systems, which can transmit only one information
stream at a specific frequency band over a specific time period, SM systems can
transmit concurrent multiple information streams. At the receiver, each antenna
receives the superposition of all transmitted information streams, which are
reflected off walls and nearby objects. Then, under certain conditions, the
transmitted information streams can be recovered by using cutting-edge
detection/decoding techniques.
Several approaches of different complexity and performance have been proposed, however, the well-known sphere decoder (SD) lies at the core of all known methods able to maximize throughput. SD is a very
promising technique able to provide the optimal solution for (traditionally NP-hard) multidimensional optimization problems, by transforming them into equivalent tree search problems. Still, the high complexity
of SD methods makes their implementation in real systems impractical when the system uses large numbers of antennas and a very high transmission rate. Current SD-based systems are, therefore, still far from
providing the performance gains predicted by theory.
The purpose of this internship is to investigate advanced approaches to efficiently traverse and narrow the corresponding SD tree search without compromising the expected SD performance. Such methods will reduce the complexity of the SD-based decoding approaches and will bring us closer to the pragmatic wireless communication able to deliver the throughputs predicted in theory.
There is a possibility that this work may lead onto a PhD position on the ERC CHAOSNETS project in the Networks Group at University College London, and partial funding for the internship itself may be available.
URL sujet détaillé :
:
Remarques :
|
|
|
|
|
|
SM207-160 Complexité implicite
|
|
|
Description
|
|
Le théorème de Rice crée une limite très forte à ce qu'on peut dire des programmes : toute propriété extensionnelle est indécidable. Autrement dit, l'équivalence "calculer la même fonction" est indécidable.
Les équivalences plus faibles n'ont que peu été étudiées. Si les équivalences syntaxiques (par exemple, "avoir autant de lignes de code") sont décidables, elles ne sont généralement pas intéressantes. De plus, elles ne sont pas des raffinements de l'équivalence extensionnelle.
Le but du stage est d'étudier les équivalences entre programmes. En particulier en cherchant à préciser l'équivalence de Rice pour chercher, notamment, à quel point on retrouve la décidabilité.
URL sujet détaillé : http://lipn.univ-paris13.fr/~moyen/stages_M2/sujBoudes-Moyen.pdf
Remarques : Co-encadrement avec P. Boudes.
|
|
|
|
|
|
SM207-161 Construction de code automodifiant
|
|
|
Description
|
|
Les virus emploient des techniques avancées pour cacher leur propre code, dans le but échapper aux logiciels d'antivirus. Sans doute l'une des plus efficace est la modification du code binaire en cours d'exécution, l'automodification. Pourtant, les virus actuels restent facilement accessible à un analyste humain. Je propose de définir un langage pour lequel une telle analyse serait bien plus difficile.
Pour cela, il faut envisager dans un premier temps de définir un langage avec de nouvelles primitives permettant de mettre en oeuvre des formes d'automodification. Viennent alors essentiellement deux problèmes: donner une sémantique (on peut penser à des continuations) et implémenter un compilateur correct relativement à la sémantique.
URL sujet détaillé : http://www.loria.fr/~bonfante/automodification.pdf
Remarques :
|
|
|
|
|
|
SM207-162 Résolution de MDP non-linéaires de grande taille, application à l'énergie.
|
|
|
Description
|
|
Planning with uncertainty.
Context:
- large scale non-linear MDP solving
- existence of approximate solvers
- existence of a platform
The first part of the work is to understand
what is MDP solving and the state of the art.
Then one of the two following goals will be
chosen:
- understanding/comparing/hybridization of
existing methods
- coarse grain parallelization
URL sujet détaillé : http://www.lri.fr/~teytaud/metis.html
Remarques : Stage rémunéré. Possibilité de continuation en thèse.
|
|
|
|
|
|
SM207-163 Nearest Neighbor Searching
|
|
|
Description
|
|
The nearest neighbor searching problem is of major importance in a variety of applications where data are represented as points in a high dimensional metric space. The metric is designed such that the distance between two points measures the similarity (or rather the dissimilarity) between the corresponding data. Examples of such applications are databases, data mining, image and video databases, ma- chine learning, clustering, quantification and data compression, pattern recognition, statistic and data analysis.
Work program:
The proposed work consists in a theoretical and experimental study of different
methods for nearest neighbor and approximate nearest neighbor searching. The set of tested methods will include, at least, the famous ANN algorithm and the compressed octree method yielding both approximate nearest neighbor searching, and a method based on a hierarchy of Delaunay graphs which provide exact nearest neighbors. Time permitting the internship student will experiment about coupling these methods with dimension reduction methods such as the Jonhson Lindenstrauss random projection method.
URL sujet détaillé : http://www-sop.inria.fr/geometrica/positions/Nearestneighbor.pdf
Remarques :
|
|
|
|
|
|
SM207-164 Rewriting methods for homology computation
|
|
|
Description
|
|
The presentations of algebras generalise the notion of rewriting systems to linear combinations of words. Given an associative algebra A on a field K, a method to compute its homology groups is to build resolutions of the ground field K by projective A-modules. Different resolutions give the same results but smaller resolutions allow faster computations of the homology groups, so that we want to build the smallest possible resolutions.
Anick proposes a procedure to compute such a resolution from a convergent presentation of the algebra. The modules of the resolution are freely generated over the =93Anick's chains=94 that correspond, in sequence, to the generators, the relations, the critical branchings (overlaps of two relations) and, for every n, the overlaps of n relations. Hence, Anick's resolution contains, for every n, relatively small data that describe all the computations on words that can be rewritten in n different ways, generalising the fact that the critical branchings give a compact description of all the words that can be rewritten in two different ways.
Anick's resolution stands as a good compromise between the =93bar resolution=94 and a minimal resolution. The =93bar resolution=94 is easy to define, since it is built from the elements of the algebra as generators and the multiplication table of the algebra as relations. However, it is intractable in practice, since it is almost always infinite. At the other end, minimal resolutions might exist but computing them is difficult in general.
The aim of this internship is to implement Anick's resolution in OCaml, together with methods for computing homological invariants of algebras induced by this resolution (Hilbert and Poincaré series, Betti numbers). This implementation will be based on the structure of linear polygraph, a unified description of presentations of monoids, categories, algebras and algebroids by higherdimensional rewriting systems, and on the homotopical reduction procedure, an explicit method to optimise the computed resolution.
URL sujet détaillé : http://math.univ-lyon1.fr/homes-www/malbos/lib/exe/fetch.php?media=stage_rshom.pdf
Remarques : Co-encadrement : Yves Guiraud (yves.guiraud.univ-paris-diderot.fr), Philippe Malbos (malbos.univ-lyon1.fr), Samuel
Mimram (samuel.mimram.fr).
|
|
|
|
|
|
SM207-165 Computation neuronale par homéostasie
|
|
|
Description
|
|
L'homéostasie est la capacité d'un système à conserver son équilibre malgré des perturbations extérieures. C'est une propriété fondamentale des êtres vivants en général, et des neurones en particulier. Par exemple, les neurones sont soumis à une activité synaptique intense, à la fois excitatrice et inhibitrice, mais leur potentiel électrique (dit potentiel membranaire) varie généralement dans un intervalle de seulement quelques millivolts. L'objet de ce stage est d'étudier l'homéostasie neuronale comme principe computationnel.
Voir sujet détaillé (url ci-dessous).
URL sujet détaillé : audition.ens.fr/brette/Stage-M2-2013-Calcul-homeostatique.pdf
:
Remarques :
|
|
|
|
|
|
SM207-166 Graphs with low forwarding index and few extra edges
|
|
|
Description
|
|
The goal is to study the following design problem : construct graphs that are as minimally congested as possible. An alternative is to study the algorithmic counterpoint : that is to find a good subgraph (inside a graph).
URL sujet détaillé : http://www-sop.inria.fr/mascotte//offres/stage_forwarding_index.pdf
Remarques : Co encadre par Frederic Gioire (CNRS).
http://www-sop.inria.fr/members/Frederic.Giroire/
|
|
|
|
|
|
SM207-167 Fractional Cops and Robber Games
|
|
|
Description
|
|
In this internship, we propose to tackle a classical combinatorial game by relaxing it into a convex game. The integral game is a pursuit game in which cops try to catch a robber inside a graph.
We hope to make progress on some on the conjectures about the cops and robber game. The scope is quite wide since there are many possible variant of the cops and robber game, moreover our convexification can be applied to others kind of games taking place in a graph.
URL sujet détaillé : http://www-sop.inria.fr/mascotte//offres/subject_cops_game.pdf
Remarques : Co encadre par Ronan Pardo Soares
http://www-sop.inria.fr/members/Ronan.Pardo_Soares
|
|
|
|
|
|
SM207-168 Adaptation structurelle au sein d'un contexte dynamique
|
|
|
Description
|
|
Mot(s)-clé(s) : Autonomic Computing, grammaire de graphe, Qualité de service, architecture distribuée
Description :
L'adaptabilité d'une application est devenue impérative dans un contexte dynamique de systèmes complexes fortement distribués et contenant un grand nombre de composants. La résolution de cette problématique peut être obtenue grâce à l'adaptation structurelle impliquant une reconfiguration de la structure architecturale de l'application. Nous nous intéressons en particulier à l'approche correcte par conception consistant à caractériser une application à l'aide d'une grammaire de graphe (ou système de réécriture de graphe). Dans ce cadre, les actions de reconfigurations sont modélisées par des règles de réécriture de graphe. Afin d'améliorer l'expressivité d'un tel système, on s'intéresse à l'implémentation des concepts de prédicats sémantiques, de mutateur et de propagation d'attributs tels qu'ils se présentent dans la théorie des grammaires "classiques" de chaîne de caractère.
Objectifs:
Le stagiaire collaborera avec les membres de l'équipe et enrichira la théorie et les modèles qui en découleront dans un premier temps. Les outils existant dans le groupe seront enrichis (GMTE, FRAMESELF) afin d'intégrer des prédicats dépendants d'éléments sémantiques dynamiques et potentiellement inconnu dans un cadre de gestion autonomique d'architecture logiciel. Pour ce faire, il sera amené à :
1) Proposer un stockage efficace d'éléments sémantiques et leur modification au travers de mutateurs arbitraires.
2) Élaborer un algorithme d'évaluation paresseux de prédicats sémantiques dépendants des éléments précédemment traités. La difficulté vient du fait que les dits éléments peuvent ne pas être connus. Les prédicats sont alors des expressions d'une logique ternaire ou infinie.
3) Étendre les outils existants afin d'intégrer des prédicats sémantiques au sein de règles de réécriture de graphe. Traiter chaque " matching " (homomorphisme de graphe attribué) de manière distribuée.
Compétences appréciées:
Logique mathématique, Théorie des graphes, Système de réécriture, Optimisation algorithmique, Programmation parallèle et concurrente, Programmation en C++.
Compétences appréciées:
- Stage indemnisé.
- Possibilité de thèse.
URL sujet détaillé : http://homepages.laas.fr/monteil/STAGES/13_grammaire.pdf
Remarques : co-encadrement avec C. Eichler
rémunération classique de stage, aide au logement si nécessaire
|
|
|
|
|
|