Centre de Recherche en Informatique

Infos générales
Liste

Liste des offres

Les offres de stage sont classées selon les catégories suivantes :

a. Analyse des langages de programmation impératifs

b. Génération de code parallèle

c. Algorithmique parallèle

d. Théorie des types

e. Divers

Offres de stage

Stage « Coarse grain loop parallelization » :

Loop parallelization is crucial for GPUs and multicore processors. Standard techniques are based on dependence graphs linking definition and usage of variable values. The graph arcs contain additional information about the relationship between loop iterations creating these arcs. This information is used to decide if the loop can be parallelized and how it should be parallelized.

The coarse grain approach does not use graphs but summaries of the loop body effects on memory. Each loop can be parallelized, regardless of its body control structure and procedure calls. Coarse grain parallelizations has already been implemented in PIPS, our automatic code analysis and transformation framework, but it should be reimplemented in a simpler way, using additional transformer information and integrating, as far as possible, auxiliary transformations such as array section privatization (this includes scalar and array privatization) and invariant code motion.

PIPS is programmed in C. It already contains lots of program analyses and transformation and is designed to be extensible. This makes adding new transformation pretty easy, once the framework is understood.

This internship requires a good C programmer, with an interest in computer architecture and code optimization, ready to interact with other PIPS developers over Internet.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech).

E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Coarse grain loop fusion » :

Loop fusion is crucial for GPU's and multicore processors with a memory hierarchy because it improves locality, sometimes dramatically. Standard techniques are based on dependence graphs linking definition and usage of variable values. The graph arcs contain additional information about the relationship between loop iterations creating these arcs. This information is used to decide if two loops can be fused and how.

The coarse grain approach does not use graphs but summaries of the loops body effects on memory. Two loops can be fused if the memory areas they write do no impact the memory area they would have read before or written after. Bascially, the Bernstein conditions must be checked for different sets of iterations and this can be performed without building a graph. Loop fusion has already been implemented in PIPS, our automatic code analysis and transformation framework, using the standard graph-based technique, but it should be reimplemented in a simpler way, using additional transformer information, allowing shifting, prologue and epilogue when the iteration sets are different, and integrating, as far as possible, auxiliary transformations such as array section privatization (this includes scalar and array privatization) and invariant code motion. Non adjacent loops should also be tackled.

PIPS is programmed in C. It already contains lots of program analyses and transformation and is designed to be extensible. This makes adding new transformation pretty easy, once the framework is understood.

This internship requires a good C programmer, with an interest in computer architecture and code optimization, ready to interact with other PIPS developers over Internet.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech).

E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Détection des variables non initialisées d'un programme C » :

La rétro-ingénierie, la maintenance et l'optimisation de codes nécessitent l'application de nombreuses analyses statiques ou dynamiques qui permettent de mieux comprendre, vérifier, améliorer et optimiser les instructions.

Parmi ces analyses, la détection des variables non initialisées avant leur utilisation permet d'éviter des erreurs lors de l'exécution du programme. Elle permet également de valider les analyses ultérieures portant sur les accès aux variables du programme, en lecture et écriture, telles que le calcul des dépendances.

La phase d'analyse dynamique de détection des variables non initialisées avant leur utilisation est déjà intégrée dans notre framework de compilation source-a-source PIPS pour des programmes en Fortran.

L'objectif de ce stage est d'implanter cette analyse pour les programmes C.

Personne à contacter : Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech).

E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Détection des débordements de tableaux d'un programme C » :

Loop parallellization is crucial for GPU's and multicore processors. Standard techniques are based on dependence graphs linking definition and usage of variable values. The graph arcs contain additional information about the relationship between loop iterations creating these arcs. This information is used to decide if the loop can be parallelized and how it should be parallelized.

The coarse grain approach does not use graphs but summaries of the loop body effects on memory. Each loop can be parallelized, regardless of its body control structure and procedure calls. Coarse grain parallelizations has already been implemented in PIPS, our automatic code analysis and transformation framework, but it should be reimplemented in a simpler way, using additional transformer information and integrating, as far as possible, auxiliary transformations such as array section privatization (this includes scalar and array privatization) and invariant code motion.

PIPS is programmed in C. It already contains lots of program analyses and transformation and is designed to be extensible. This makes adding new transformation pretty easy, once the framework is understood.

This internship requires a good C programmer, with an interest in computer architecture and code optimization, ready to interact with other PIPS developers over Internet.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech). E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Coarse grain loop fusion » :

Loop fusion is crucial for GPU's and multicore processors with a memory hierarchy because it improves locality, sometimes dramatically. Standard techniques are based on dependence graphs linking definition and usage of variable values. The graph arcs contain additional information about the relationship between loop iterations creating these arcs. This information is used to decide if two loops can be fused and how.

The coarse grain approach does not use graphs but summaries of the loops body effects on memory. Two loops can be fused if the memory areas they write do no impact the memory area they would have read before or written after. Bascially, the Bernstein conditions must be checked for different sets of iterations and this can be performed without building a graph. Loop fusion has already been implemented in PIPS, our automatic code analysis and transformation framework, using the standard graph-based technique, but it should be reimplemented in a simpler way, using additional transformer information, allowing shifting, prologue and epilogue when the iteration sets are different, and integrating, as far as possible, auxiliary transformations such as array section privatization (this includes scalar and array privatization) and invariant code motion. Non adjacent loops should also be tackled.

PIPS is programmed in C. It already contains lots of program analyses and transformation and is designed to be extensible. This makes adding new transformation pretty easy, once the framework is understood.

This internship requires a good C programmer, with an interest in computer architecture and code optimization, ready to interact with other PIPS developers over Internet.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech). E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Détection des variables non initialisées d'un programme C » :

La rétro-ingénierie, la maintenance et l'optimisation de codes nécessitent l'application de nombreuses analyses statiques ou dynamiques qui permettent de mieux comprendre, vérifier, améliorer et optimiser les instructions.

Parmi ces analyses, la détection des variables non initialisées avant leur utilisation permet d'éviter des erreurs lors de l'exécution du programme. Elle permet également de valider les analyses ultérieures portant sur les accès aux variables du programme, en lecture et écriture, telles que le calcul des dépendances. La phase d'analyse dynamique de détection des variables non initialisées avant leur utilisation est déjà intégrée dans notre framework de compilation source-a-source PIPS pour des programmes en Fortran.

L'objectif de ce stage est d'implanter cette analyse pour les programmes C.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech). E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Détection des débordements de tableaux d'un programme C » :

La rétro-ingénierie et la maintenance de codes nécessitent l'application de nombreuses analyses statiques ou dynamiques qui permettent de mieux comprendre et de vérifier les programmes.

Parmi ces analyses, la détection des débordements de tableaux est essentielle. Elle permet d'éviter des erreurs lors de l'exécution du programme, mais aussi de valider les résultats des analyses qui caractérisent l'ensemble des éléments de tableaux référencés par des instructions. La phase d'analyse dynamique de détection des débordements de tableaux est déjà intégrée dans notre framework de compilation source-a-source PIPS pour des programmes en Fortran.

L'objectif de ce stage est d'implanter cette analyse pour les programmes C.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech). E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Linéarisation de tableaux et test de dépendance » :

PIPS est un framework de compilation source-a-source qui intègre de nombreuses transformations de programmes source-a-source ainsi que des analyses statiques et dynamiques et qui permet d'en développer rapidement de nouvelles.

Une des optimisations clés est la parallélisation automatique de boucles. Mais les programmeurs C ainsi que les générateurs automatiques de code C ont tendance à linéariser leurs tableaux, c'est-à-dire à remplacer les tableaux multidimensionnels par des tableaux monodimensionnels. Les expressions d'indices qui en résultent ne sont généralement pas affines et les tests de dépendance échouent. L'objectif de ce stage est de développer un nouveau test de dépendance permettant de linéariser, dans le vrai sens du terme, les polynomes qui résultent d'une linéarisation de tableaux. Un minimum de connaissance en algèbre linéaire permettra d'aborder le sujet plus facilement.

Ce stage est plutôt orienté ingénieur, mais il peut éventuellement se prolonger par une thèse dans le domaine de la compilation.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech). E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Ordonnancement optimal et vectorisation des calculs de l'opérateur de Dirac » :

La Chromodynamique Quantique sur Réseaux (Lattice Quantum ChromoDynamics ou LQCD en anglais) étudie le mécanisme de la formation de la matière à travers l'interaction des particules fondamentales de l'univers sous les contraintes de confinement (naissance de l'univers juste après le Big Bang). Un axe très prépondérant de cette étude repose sur d'intenses simulations (de type Monte Carlo), dont le principal ingrédient est l'opérateur de Dirac. Du point de vue informatique, la mise en œuvre de cet opérateur expose des patterns d'accès mémoire assez spéciaux ainsi qu'un schéma de calcul pouvant contenir des redondances. L’évaluation de l'opérateur de Dirac étant très répétée, sa mise en œuvre optimisée (suivant l'architecture cible) est devenue le principal cheval de bataille dans la recherche en LQCD (voir le projet PetaQCD financé par l'Agence Nationale de le Recherche).

L'étude d'une mise en œuvre efficace de l'opérateur de Dirac se fait à deux niveaux. Le niveau macroscopique, dans lequel le réseaux global est subdivisé en sous-réseaux géométriquement identiques, il faut donc trouver le bon partitionnement et gérer efficacement les communications entre les sous-réseaux. Le niveau microscopique, dans lequel on réorganise les calculs de base de l'opérateur proprement dit de manière à réduire les redondances tout en limitant la perte d'efficacité mémoire (défaut de caches). Cette réorganisation peut se faire par des approches algébriques (factorisations et simplifications en algèbre linéaire) et/ou par une réécriture des instructions de manière à utiliser plus efficacement les possibilités de l'architecture cible (pipeline d'instructions, vectorisation).

Le travail ici consistera à transformer le corps de la boucle principale de l'opérateur de Dirac, de manière à réduire au mieux les défauts de cache. On pourra utiliser un modèle analytique (à déterminer) ou un outil approprié pour mesurer l'efficacité mémoire. La vectorisation explicite du code sera ensuite envisagée.

Prérequis : Un minimum de connaissance en algèbre linéaire et optimisation de code facilitera l'entrée en matière pour ce sujet. De plus, un intérêt pour l'adéquation application/code/architecture sera utile pour entretenir un bon degré de motivation et d'enthousiasme. Il n'est pas nécessaire d'avoir des connaissances en physique des particules, mais un minimum de culture sur le sujet sera acquis en chemin. Ce stage, qui pourra être mené aussi bien sous un angle recherche que sous un angle programmation, pourra servir de point de départ pour une thèse en calcul haute performance (pour la QCD).

Personne à contacter :

Envoyer un CV et une lettre de motivation à Claude Tadonki (CRI, MINES ParisTech). E-mail : claude.tadonki--at--mines-paristech.fr Web : http://www.omegacomputer.com/staff/tadonki/

Stage « Représentations intermédiaires parallèles pour LLVM et GCC » :

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.

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.

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.

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.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Pierre Jouvelot (CRI, MINES ParisTech). E-mail : pierre.jouvelot--at--mines-paristech.fr Web : http://www.cri.mines-paristech.fr/~pj

Stage « Multithreading sous Matlab » :

Sujet : Multithreading sous Matlab (Stage Master Recherche 2012/2013)

Projet : 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.

Descriptif : 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.

Exigences : 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.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Claude Tadonki (CRI, MINES ParisTech). E-mail : claude.tadonki--at--mines-paristech.fr Web : http://www.omegacomputer.com/staff/tadonki/

Stage « Mise en oeuvre efficace d'algorithmes d'inondation sur des grandes images à niveaux de gris » :

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 noeuds 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 coeurs 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 oeuvre sur processeurs vectoriels ou graphiques. Contacts:

Personnes à contacter :

Envoyer un CV et une lettre de motivation à Fernand Meyer (fernand.meyer--at--mines-paristech.fr) et Claude Tadonki (claude.tadonki--at--mines-paristech.fr)

Stage « Mise en oeuvre efficace d'un système de localisation de texte enfoui dans des images ordinaires » :

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'École 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.

Exigences : 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-coeurs 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à.

Personnes à contacter :

Envoyer un CV et une lettre de motivation à Beatriz Marcotegui (beatriz.marcotegui--at--mines-paristech.fr) et Claude Tadonki (claude.tadonki--at--mines-paristech.fr)

Stage « Reconstruction d'images à grande échelle sur GPU » :

Description du stage : Dans le contexte de la simulation de forage, la reconstruction d'une vue principale à partir de vues partielles est une opération importante et récurrente. En plus de la complexité fondamentale de l'algorithme considéré, il faut ajouter celle liée à la résolution des images traités. Comme la plupart des modules de traitement d'images, l'accélération à l'aide de GPUs est devenu un recours naturel. Toutefois, sachant que le principal goulot d'étranglement en ce concerne les GPUs c'est la mémoire et les échanges avec le CPU, la considération des scénaris à grande-échelle (taille et/ou résolution) à performance quasi-constante est un défi technique à étudier. Le but du présent stage est d'explorer les possibilités de mise en oeuvre efficace de la reconstruction d'images à grande échelle sur les GPUs de dernière génération. Le travail débutera par le déploiement et le profilage du module existant, suivi d'une extension pour la prise en compte des résolutions élevées. La mise au point pourra se faire sur les GPUs disponibles, le passage au GPU Pascal par exemple se fera par la suite.

Exigences :

Le candidat devrait avoir un bon niveau en programmation C et quelques notions de traitement d'images. Des bases en programmation GPU seraient un plus.

Personnes à contacter :

Envoyer un CV et une lettre de motivation à Claude Tadonki (claude.tadonki--at--mines-paristech.fr) et Olivier Stab (olivier.stab--at--mines-paristech.fr)

Stage « Maude in Dedukti » :

Context : Dedukti is a type-checker for the lambda-Pi calculus modulo, a type system characterized by two features: dependent types and a conversion rule generated by beta-reduction and rewriting modulo a given set of rewrite rules Preliminary experiments have shown that the reduction algorithm (a modi cation of the virtual machine of Matita that takes into account rewrite rules) behaves well on simple examples coming from Rewriting Logic and has comparable results to Maude.

Subject : The aim of this internship is to go further in this direction, by de ning a transla- tion from Rewriting Logic into Dedukti's format, and by improving the reduction algorithm of Dedukti to become competitive on the whole set of problems with respect to Maude.

Prerequisites : An advanced course on the fundations of computer science such as logic, type theory or rewrite systems. A compiler course would be a plus

Environment : The intern will be hosted by the Deducteam project-team at Inria Paris-Rocquencourt and/or the CRI at MINES ParisTech.

**More information in this file.

Personnes à contacter** :

Envoyer un CV et une lettre de motivation à Olivier Hermant(olivier.hermant--at--mines-paristech.fr)

Stage « Normalization by Completeness » :

Context : Proofs of cut elimination have took two di erent ways for a long time: syntac- tic cut reduction and proofs that this process terminates, and semantic proofs of cut admissiblity. Recent works tend to show that some unity exist between two methods. The goal of this project is therefore to compare those two approaches, and more speci cally, to force cut admissibility to generate proofs in normal form that are reducts of the original proofs via an adequate reduction relation. The main framework of interest of this internship will be Deduction Mod- ulo, that provides in particular a uni ed way to study axiomatic theories and axiomatic cuts.

Subject : The internship will rst focus on the study of the pair of theorems soundness/(cut- free) completeness, and on the computational content of such a cut admissibility proof. This can for instance be made through a formalization in a (construc- tive) proof-assistant of the propositional fragment, as did Hugo Herbelin for completeness with respect to Kripke structures. The next steps will depend on the interests an results of the candidate. That could be for instance:

- carrying the initial proof (in sequent calculus, natural deduction, ...) through soundness and completeness in order to make a formal link between the original proof and the cut-free proof obtained at the very end. - model transformations that go from Heyting algebras to (extensions of) Kripke structures, in order to compare this work to Normalization by Evaluation. This last step will take us into the world of proof normalization, while we have started by pure semantic proofs of cut admissibility

Prerequisites : At least one advanced course on the fundations of computer science such as logic or type theory. Some notions of category theory would be a plus.

Environment : The intern will be hosted by the Deducteam project-team at Inria Paris-Rocquencourt and/or the CRI at MINES ParisTech.

**More information in this file.

Personnes à contacter** :

Envoyer un CV et une lettre de motivation à Olivier Hermant(olivier.hermant--at--mines-paristech.fr)

Stage « Parallélisme et distribution de calculs paramétriques sur cluster HPC » :

Contexte : EDF R&D a pour missions principales de contribuer à l’amélioration de la performance des unités opérationnelles du Groupe EDF, d’identifier et de préparer les relais de croissance à moyen / long termes. Au sein d'EDF R&D, le département PERICLES (Performance et Prévention des Risques Industriels du Parc par la Simulation et les Etudes) est pôle de compétence dans les domaines de la physique des réacteurs nucléaires, du développement des codes de calcul et des systèmes d'information, de la visualisation, des risques industriels, de la cybersécurité, des facteurs humains.

Lors de votre stage, vous rejoindrez une équipe de recherche et d’études « Architecture, Système d'Information et Calculs Scientifique » (groupe ASICS) du département PERICLES spécialisée dans l’architecture des systèmes d’information et le calcul scientifique, avec applications au calcul haute performance (HPC) entre autres, et ce au service des projets du Groupe EDF. L’équipe ASICS contribue au développement d’un Jumeau Numérique de réacteur à partir des briques logicielles de de la plateforme de simulation SALOME open source permettant d’effectuer une étude numérique physique avancée. Le Jumeau Numérique de réacteur a pour objectif de fournir aux ingénieurs et exploitants un environnement intégré de visualisation des phénomènes physiques complexes leur permettant d’aboutir à une simulation rapide et de plus en plus prédictive. Le stage proposé est en lien avec la réalisation de ce Jumeau Numérique en cours de développement.

Missions: [...] Dans le cadre de la plateforme de simulation SALOME composée d’un certain nombre de modules (CAO, Maillage, Gestion de Calcul, Visualisation, etc.), les ingénieurs du Groupe EDF sont amenés à effectuer des études paramétriques basées sur différents modèles physiques produits à l’aide des codes de calcul « maison ». Il s’agit des études avancées dans le cadre des simulations couvrant différents champs d’application : neutronique (coeur du réacteur), mécanique et thermodynamique des installations, phénomènes d’électromagnétisme, etc.

Les études paramétriques, notamment les calculs de l’incertitude, prévues dans le contexte des études de sûreté pour le parc nucléaire, sont souvent réalisées à l’aide de la bibliothèque OpenTurns couplée à SALOME (http://openturns.github.io/). Le module YDEFX de SALOME permet de gérer les calculs paramétriques à réaliser (par exemple, lancement et suivi de calculs à distance, récupération des résultats) où la fonction d'étude est exprimée en langage Python. Ce module dispose d’une implémentation informatique basée sur un outil « maison » appelé YACS dans la plateforme SALOME et destiné à l’exécution des schémas de calculs dans un environnement distribué HPC. L’objectif de ce stage est d'étudier des solutions alternatives à YACS pour l’implémentation des calculs paramétriques respectant les spécifications d’YDEFX, au moyen d'outils qui viennent du monde Python (modules dispy, pycos, pathos). D'autres outils et langages (Julia, Rust,..) pourraient éventuellement être envisagés. Plus d'informations dans ce fichier.

Déroulement du stage : Le (la) stagiaire sera amené(e) à travailler sur les volets suivants :

  • Prise en main de l’existant (couple SLURM/YACS, fonctionnement d’un cluster HPC),
  • Évaluation des capacités / limites du couple SLURM/YACS,
  • Proposition et expérimentation des solutions alternatives,
  • Rédaction d’un document de synthèse comparant sous angle critique différentes solutions étudiées,
  • Production d’un prototype répondant à des contraintes YDEFX, avec validation sur un cas d’application physique (neutronique, thermique ou mécanique…).

Une part importante du travail consistera à découvrir, étudier et assimiler divers outils informatiques et technologies orientés HPC. S’agissant des travaux de développement, à l’issue de ce stage, des travaux de recherche plus approfondis (sous forme de thèse), orientés parallélisme gros grain et distribution de calculs, pourraient être envisagés. La motivation du (de la) candidat(e) sera évaluée en ce sens.

Profil recherché : Elève-ingénieur en dernière année ou Master 2 spécialisé en informatique, en particulier Calculs HPC. Compétences techniques recherchées :

  • bonne connaissance de la conception orientée objet et de l'environnement Linux,

  • pratique Python et C++,

  • maîtrise des méthodes de distribution et de parallélisation de calculs.

Autres compétences indispensables :

  • motivation et curiosité, force de proposition,
  • autonomie et capacité d'auto-formation, capacités d’analyse et de synthèse,
  • esprit critique et démarche expérimentale, appétence pour la recherche en informatique,
  • qualité rédactionnelle ainsi que maîtrise de l'anglais technique.

Formalités de stage : Durée : 5-6 mois Lieu : EDF R&D - EDF Lab Paris-Saclay (Palaiseau) Stage rémunéré : oui Contact : ingénieurs-chercheurs à EDF R&D M. O. MIRCESCU (ovidiu.mircescu@edf.fr) et M. F. GOUIN (florian.gouin@edf.fr) Corinne Ancourt (CRI, MINES ParisTech) (corinne.ancourt--at--mines-paristech.fr).

Stage « Modèle de Données Métier : Application jumeau numérique » :

Contexte : EDF R&D a pour missions principales de contribuer à l’amélioration de la performance des unités opérationnelles du Groupe EDF, d’identifier et de préparer les relais de croissance à moyen / long termes. Au sein d'EDF R&D, le département PERICLES (Performance et Prévention des Risques Industriels du Parc par la Simulation et les Etudes) est pôle de compétence dans les domaines de la physique des réacteurs nucléaires, du développement des codes de calcul et des systèmes d'information, de la visualisation, des risques industriels, de la cybersécurité, des facteurs humains.

Lors de votre stage, vous rejoindrez une équipe de recherche et d’études « Architecture, Système d'Information et Calculs Scientifique » (groupe ASICS) du département PERICLES spécialisée dans l’architecture des systèmes d’information et le calcul scientifique, avec applications au calcul haute performance (HPC) entre autres, et ce au service des projets du Groupe EDF. L’équipe ASICS contribue au développement d’un Jumeau Numérique de réacteur à partir des briques logicielles de de la plateforme de simulation SALOME open source permettant d’effectuer une étude numérique physique avancée. Le Jumeau Numérique de réacteur a pour objectif de fournir aux ingénieurs et exploitants un environnement intégré de visualisation des phénomènes physiques complexes leur permettant d’aboutir à une simulation rapide et de plus en plus prédictive.Le stage proposé est en lien avec la réalisation de ce Jumeau Numérique en cours de développement.

Missions: L'ingénierie dirigée par les modèles (IDM ou model-driven engineering) est un ensemble de pratiques fondées sur le concept de modèle de données. Ces pratiques ont pour but d'automatiser la production, la maintenance ou l'utilisation de systèmes logiciels en s’appuyant sur les techniques de modélisation, de transformation de modèle et de génération automatique de code. Dans le contexte de la plateforme Jumeau Numérique de réacteur, les modèles de données sont générés en XSD (XML Schema Definition) par l’outil MDM. La structuration forte et la validation des données sont des préalables indispensables pour l’exécution des solveurs et des workflows associés. Le Web Ontology Language (OWL), défini par le W3C, est une famille de langages de représentation des connaissances pour la création d'ontologies formelles Ces ontologies sont actuellement la pierre angulaire des pratiques d'échange de données et des normes d'interconnexion du Web sémantique. Dans le cadre de la transformation automatique de modèles, l’objectif est d’établir une passerelle entre les modèles utilisant une approche ontologique OWL et ceux utilisant une formalisation XSD. Par conséquent, en ce qui concerne les modèles, il faut être en mesure de convertir/générer un schéma XSD en une ontologie OWL et réciproquement. Pour les données, il faut être en mesure de convertir des documents XML valides en données RDF pour le peuplement de l'ontologie et réciproquement. Il serait donc nécessaire d’établir des liens bidirectionnels entre les individus d'une base de connaissances classifiée et typée à l'aide d'une ontologie et les informations de documents XML respectant un modèle XSD.

Déroulement du stage : Le (la) stagiaire sera amené(e) à travailler sur les volets suivants :

  • Identification de couples de patterns (XSD, OWL),
  • Définition d’une méthodologie de conversion bidirectionnelle,
  • Automatiser le plus possible le/les processus de conversion(s) des modèles et des données grâce à un formalisme implémentant la méthodologie.

Le modèle de données utilisé par le Réacteur Numérique servira de cas d’usage.

Profil recherché : Elève-ingénieur en dernière année ou Master 2 spécialisé en informatique. Compétences techniques recherchées :

  • ingénierie du logiciel, notions de modélisation de données,

  • Langage python

  • connaissances XSD et/ou OWL

Autres compétences indispensables :

  • motivation et curiosité, force de proposition,
  • autonomie et capacité d'auto-formation, capacités d’analyse et de synthèse,
  • esprit critique et rigueur,
  • qualité rédactionnelle ainsi que maîtrise de l'anglais.

Formalités de stage : Durée : 5-6 mois Lieu : EDF R&D - EDF Lab Paris-Saclay (Palaiseau) Stage rémunéré : oui Contact : ingénieurs-chercheurs à EDF R&D M. E. FAYOLLE (eric.fayolle@edf.fr) et Mme P. NOYRET (pascale.noyret@edf.fr) Corinne Ancourt (CRI, MINES ParisTech) (corinne.ancourt--at--mines-paristech.fr).

Stage « Utilisation de l’Intelligence Artificielle pour la détection de piétons dans des scènes denses » :

Contexte : Les méthodes d'intelligence artificielle et plus particulièrement l'apprentissage profond (Deep Learning) ont permis de réaliser des progrès notoires dans le domaine du traitement d'images. En effet, plusieurs techniques à base de réseaux de neurones ont été proposés pour améliorer la détection des objets. Elles ont même permis de dépasser, sous certaines conditions, les performances de l'être humain. Cependant, l’apprentissage profond est moins efficace quand il s'agit de cas compliqués, comme pour les scènes denses avec présence d'occlusion.

Missions: L'objectif du stage est d'adapter des techniques récemment développées pour traiter ces cas complexes et de les tester pour la détection de piétons dans des scènes denses. Les expériences seront menées sur une architecture matérielle comprenant un GPU performant.

Profil recherché : Ce stage requiert de bonnes compétences en programmation Python, avec un intérêt pour les techniques d’Intelligence Artificielle et de traitement d’images.

Formalités de stage : Le lieu du stage est : Centre de recherche en informatique MINES ParisTech 35 rue Saint-Honoré 77305 Fontainebleau Cedex Le CRI est facilement accessible depuis Paris par train depuis la gare de Lyon ; il y a un train toutes les 30 minutes et il faut compter 40 minutes de transport. Une fois à la gare de Fontainebleau, on peut emprunter un bus municipal (Ligne 1).

Personne à contacter : Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech). E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Instrumentation d’un outil de simulation géologique » :

Contexte : La modélisation numérique des problèmes physiques permet de mieux comprendre la complexité des processus qui sont inaccessibles et impossibles à reproduire précisément par les moyens expérimentaux ou par les méthodes analytiques. HYTEC, développé au Centre de Géosciences de MINES ParisTech depuis 1994, est un code de transport réactif qui rassemble la modélisation des processus thermodynamiques, hydrodynamiques et chimiques (THC) en milieu poreux, et qui s’applique par exemple au stockage de CO2 ou à la récupération in situ de minerai. Au-delà de l’application et de la modélisation, une expertise du code (en C++) est nécessaire à plusieurs niveaux, du point de vue langage.

Missions: Toutes les informations sont dans ce fichier.

Formalités de stage : Le lieu du stage est : Centre de recherche en informatique et Centre de Géosciences MINES ParisTech 35 rue Saint-Honoré 77305 Fontainebleau Cedex Le CRI est facilement accessible depuis Paris par train depuis la gare de Lyon ; il y a un train toutes les 30 minutes et il faut compter 40 minutes de transport. Une fois à la gare de Fontainebleau, on peut emprunter un bus municipal (Ligne 1).

Personne à contacter : Envoyer un CV et une lettre de motivation à Olivier Hermant (CRI, MINES ParisTech). E-mail : olivier.hermant--at--mines-paristech.fr

Université PSLInstitut Mines-TelecomParisTechCarnot M.I.N.E.SArmines