Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)
    ===== Internships 2014/2015 =====

Submit an internship offer

  1. A dynamical system approach to compute the transient behavior of stochastic distributed systems.
    Nicolas Gast, Bruno Gaujal. Inria Grenoble
    2.17.1 (network modeling) and 2.18.1 (Distributed Algorithms for Networks)
  2. Vehicle Sharing Systems: Analysis, modeling, simulation, optimization
    Nicolas GAST - INRIA Monbonnot and Vincent JOST - CNRS G-SCOP Grenoble
  3. Calcul efficace de coefficients de séries
    Frédéric Chyzak et Alin Bostan - INRIA Saclay ÎDF (à Palaiseau)
  4. Preuves algorithmiques pour la transcendance des séries
    Frédéric Chyzak et Alin Bostan - INRIA Saclay ÎDF (à Palaiseau)
  5. FouCo : support pour les définitions corécursives dans l'assistant de preuves Isabelle/HOL
    Jasmin Blanchette - Inria Nancy ou Max-Planck-Institut für Informatik à Sarrebruck (Allemagne)
    1-20, 1-22, 1-36, 2.5.1, 2.7.2, 2.36.1
  6. Relativized Implicit Computational Complexity and Declassification
    Frédéric Prost - LIP ENS-Lyon
    2.1 / 2.6 /
  7. Translation methods for deciding separation logics
    Stéphane Demri – LSV, ENS Cachan
    2.5.1, 2.9.1, 2.9.2, 2.36.1
  8. www.prism.uvsq.fr/~ystr/stage.html
    Laboratoire PRiSM, Université de Versaille Saint QUentin
    Techniques de théorie des jeux en informatique
  9. Verification of Distributed Systems with Parameterized Network Topology
    Benedikt Bollig & Paul Gastin (LSV, ENS Cachan)
    2-3; 2-8; 2-9; 2-16; 2-20
  10. Études des algorithmes pour différentes classes de jeux stochastiques, jeux représentés implicitement
    Yann Strozecki, Université de Versailles Saint Quentin, PRiSM
    Techniques de théorie des jeux en informatique
  11. Complexité d'énumération : séparation de classes et bornes inférieures
    Yann Strozecki, Université de Versailles Saint Quentin, PRiSM
    2.26.1, 2.31.1, 2.33.1
  12. Highly Concurrent Data Structures
    Petr Kuznetsov, ENST
    2.3
  13. Arrangements of DP-ribbons
    Michel Pocchiola (Paris 6) & Vincent Pilaud (École Polytechnique)
    2-38-1
  14. Multitriangulations de surfaces
    Vincent Pilaud (École Polytechnique)
    2-38-1
  15. Optimisation et réécriture de requêtes sous constraintes : Graphes , Arbres et mots
    Sophie Tison et Pierre Bourhis - LIFL & INRIA LILLE
    1-18; 2.16; 2.26.1; 2.26.2
  16. Distributed Algorithms Run By Selfish Agents
    Pierre Fraigniaud and Paolo Penna, LIAFA, Univ. Paris Diderot
    2.18.1
  17. Exploring the Limits of Distributed Computation: Local Graph Coloring
    Pierre Fraigniaud and Adrian Kosowski, LIAFA, Univ. Paris Diderot
    2.18.1
  18. Decision procedures for FOLTL
    Julien Brunel - ONERA - Toulouse
  19. Temporal multi-agent logic for requirement modelling
    Julien Brunel - ONERA - Toulouse
  20. Plongements topologiques de graphes dans des 2-complexes simpliciaux
    Éric Colin de Verdière - ENS Ulm (Paris 5ème)
    2-38-1, 2-29-1, 2-14-1
  21. Décroisements de graphes dans le plan avec obstacles
    Éric Colin de Verdière - ENS Ulm (Paris 5ème)
    2-38-1, 2-29-1, 2-14-1
  22. Approche par contrats pour la sûreté de fonctionnement dans les systèmes critiques "cyber-physiques"
    Daniela Cancila - CEA Saclay, Nanoinnov
    2.3, 2.16, 2.23.1, 2.36.1, 2.37.1
  23. Verifying replicated data structures: causal consistency
    Ahmed Bouajjani and Constantin Enea - LIAFA, Univ. Paris Diderot
    2.3 - 2.9.2 - 2.18.2
  24. Verification of Haskell Programs
    Matthew Hague, Royal Holloway University of London
    1-22, 2.4, 2.6, 2.9.1, 2.9.2, 2.16
  25. Version management for big-data storage
    Marc Shapiro, LIP6 (Paris)
  26. PiCoq: pi-calculus within Coq
    Damien Pous, LIP, ENS Lyon
  27. Calcul sécurisé efficace et sûr
    Julien Bringer - Morpho - Issy-Les-Moulineaux
    2.12 2.13 2.30
  28. Calcul vérifiable pour la biométrie
    Julien Bringer - Morpho - Issy-Les-Moulineaux
    2.12 2.13 2.30
  29. Type refinement in λΠ-calculus modulo
    Arnaud Spiwack & Olivier Hermant – Deducteam, Inria Paris-Rocquencourt & CRI, MINES ParisTech
    2.7.1, 2.7.2, 2.1, 2.4
  30. From Completeness to Normalization
    Olivier Hermant (Mines and Inria Paris)
    2.7.1 (Foundations of Proof Systems) and 2.7.2 (Proof Assistants)
  31. Compilation certifiée de réseaux de Petri colorés
    Frédéric Gava (LACL) et Franck Pommereau (IBISC)
  32. Implantation distribué de modèles concurrents
    Frédéric Gava (LACL) et Franck Pommereau (IBISC)
  33. Vérification d'algorithmes de Model checking
    Frédéric Gava et Julien Tesson (LACL)
  34. QuickChick: Property-Based Testing for Coq
    Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)
    1-20, 1-22, 1-24, 1-31, 2.1, 2.4, 2.5.1, 2.6, 2.7.1, 2.7.2, 2.36.1
  35. Erreurs d'arrondi en analyse numérique
    Sylvie Boldo - Inria Saclay
    2.7.2 2.36.1
  36. Querying Probabilitistic Data via Tree Decompositions
    Pierre Senellart - Télécom ParisTech & National University of Singapore
    2.26.2, 2.26.1, 2.16
  37. Canonical form of Boolean network & properties
    Franck Delaplace - IBISC LAB, Tarek Melliti - IBISC LAB
    I32,
  38. 3D Time-Traveler: Interpolation Interactive 3D+T
    Julien Tierny _julien.tierny@lip6.fr_, Julie Delon _julie.delon@parisdescartes.fr_, Sorbonne Universites UPMC - LIP6, Paris (Metro 7,10)
  39. inSitu Topology: Visualisation pour le Calcul Haute Performance
    Julien Tierny _julien.tierny@lip6.fr_, Sorbonne Universites UPMC - LIP6, Paris (Metro 7, 10)
  40. Construction de graphes de Reeb et squelettes topologiques pour la visualisation des champs scalaires dans le logiciel Open-Source ParaView
    Alejandro Ribes _alejandro.ribes@edf.fr_, Julien Tierny _julien.tierny@lip6.fr_, EDF Clamart
  41. Proof of convergence for a spacecraft guidance rendezvous algorithm
    M. Joldes, C. Louembet - LAAS-CNRS, Toulouse
  42. Étude combinatoire d'arbres et d'arrangements d'hyperplans
    Sylvie Corteel (LIAFA Universite Paris Diderot et David Forge (LRI, Universite Paris Sud)) corteel@liafa.univ-paris-diderot.fr, forge@lri.fr
    C2-10
  43. Étude logique de l'ordonnancement dans les algèbres de processus
    Emmanuel Beffara - LIP, ENS Lyon
    1.20, 2.1, 2.2, 2.3, 2.4
  44. Define an internalization of Homotopy Type Theory in Coq
    N. Tabareau/M. Sozeau - Inria, Nantes-Paris
    2.7.2
  45. Define and implement a general notion of higher inductive types
    N. Tabareau/M. Sozeau - Inria, Nantes-Paris
    2.7.2
  46. Parallel algorithms for geometric information analysis from 3D scanners
    Sylvain Contassot-Vivier and Adrien Krähenbühl - LORIA Nancy
  47. Proof-Theoretic Strengh of MSO on Infinite Words
    Colin Riba – LIP - ENS de Lyon
    2.16, 2.20.2
  48. Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
    Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)
    2.4, 2.5.1, 2.6, 2.7.2, 2.36.1
  49. Étude de la résistance des algorithmes de cryptographie légère face aux attaques physiques
    Jacques Fournier - CEA LSAS, Centre Micro-électronique de Provence, Gardanne (13)
    2.13.2 et 2.12.1
  50. Information per time unit in timed systems
    E. Asarin and A. Degorre - LIAFA
    2-8-2
  51. Compression of mixed (discrete-continuous) signals
    E. Asarin and A. Degorre - LIAFA
    2-8-2
  52. Optimal mechanisms for the protection of confidential information
    Catuscia Palamidessi and Konstantinos Chatzikokolakis. INRIA and Ecole Polytechnique
  53. Topology of singular curves and surfaces
    Guillaume Moroz et Marc Pouget
    ALGO COCA 2.22 2.13.1
  54. Standardisation in the linear substitution calculus
    Delia Kesner - PPS - Univ. Paris-Diderot
  55. Analyse de la sécurité d'algorithmes de chiffrement authentifié
    Thomas Fuhr et Henri Gilbert - ANSSI, Paris
  56. Verified JIT compilation of Coq
    Xavier Leroy, Maxime Dénès – Inria Paris-Rocquencourt
    2-4, 2-7-1, 2-7-2
  57. Vérification formelle d’analyses de complexité
    Francois Pottier et Arthur Charguéraud, INRIA Paris-Rocquencourt
    2.4, 2.7.2, 2.36.1
  58. Games of imperfect information over graphs
    Patricia Bouyer (LSV), Samson Lasaulce (L2S), Nicolas Markey (LSV)
    2.20.1, 1.22, 1.24
  59. Vérification de preuves d'arithmétique dans le lambda-Pi-calcul modulo
    David Delahaye - Inria Paris (Place d'Italie)
    2.5.1, 2.7.1, 2.7.2, 2.36.1
  60. Une approche inspirée de l'archéologie pour l'analyse de données de votes dans une élection
    Olivier Spanjaard, Fanny Pascual - Sorbonne Universités Univ Paris 06, Laboratoire d'Informatique de Paris 6
    Algorithmique, optimisation combinatoire, complexité
  61. Analyse fonctionnelle en Coq
    Sylvie Boldo - Inria Saclay
    2.7.2
  62. Algorithmic issues in MapReduce
    E. Bampis, G. Lucarelli, D. Trystram - INRIA Grenoble or LIP6
    2.24.1, 2.29.1
  63. conception et la programmation d'algorithmes de reconstruction de codes correcteurs d'erreurs
    Pierre Loidreau - Direction générale de l'armement (Rennes)
    2.13.2
  64. F*: SMT-Based Verification for ML
    Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)
    2.4, 2.7.2, 2.36.1, 2.5.1, 2.7.1, 2.6, 2.1
  65. Inférence de modèle réactionnel correspondant à un graphe d’influence
    François Fages et Sylvain SOliman - Inria Paris-Rocquencourt
    C2.19, C2.6
  66. Boolean models of biochemical reactions
    François Fages - Inria Paris-Rocquencourt
    C2-19, C2.6
  67. Proof Engineering Tools for Coq
    Eelco Visser and Pierre Neron and Andrew Tolmach - TU Delft - Netherlands)
    2.7.2 2.4
  68. Formal Study of a Countermeasure Against Side-Channel Attacks
    Pablo Rauzy and Sylvain Guilley, at Télécom ParisTech
  69. Protecting Elliptic Curve Cryptography Against Fault Injection Attacks
    Pablo Rauzy and Sylvain Guilley, at Télécom ParisTech
  70. Formalizing Functions as Processes
    Beniamino Accattoli - INRIA Saclay, Parsifal Team
  71. A weakly relational domain to detect potential polymerisation events in signaling pathways
    J Feret, DI - Ecole normale supérieure, 75005 Paris
    M2 - 6: Abstract interpretation
  72. Approximate model reduction for the differential semantics of rule-based models
    J Feret, DI - Ecole normale supérieure, 75005 Paris
    M2 - 6: Abstract interpretation
  73. Algorithmes de Partitionnement de Graphes Dynamiques - Dynamic Graphs Partitionning Algorithms
    Nicolas Schabanel - LIAFA (U. Paris Diderot)
    2.11.1, ,1.24, 2.11.2, 2.18.1, 2.24.1, 2.29.1, 2.38.1
  74. Functional Programming and Operating System research
    Thomas Gazagnaire - University of Cambridge
  75. Gelfand duality for compact partially ordered spaces
    Emmanuel Haucourt - École Polytechnique (LIX)
    Concurrency 2.3
  76. almost free categories
    Emmanuel Haucourt - École Polytechnique (LIX)
    Concurrency 2.3
  77. Sémantique opérationnelle catégorique
    Tom Hirschowitz - Chambéry
    1-20;2.2;2.3
  78. Résolution de contraintes pour la vérification de programmes
    Sébastien Bardin, CEA LIST (Paris-Saclay)
  79. Génération de tests structurels pour des critères avancés
    Sébastien Bardin, Nikolay Kosmatov, CEA
  80. Réalisation d'outils pour le décodage d'exécutables
    Sébastien Bardin, CEA LIST (Paris-Saclay)
  81. Génération automatique d'exploits à partir de traces d'erreurs
    Marie-Laure Potet, Laurent Mounier (Verimag), Sébastien Bardin (CEA)
  82. Negotiation of correspondence policies
    A.Bouabdallah - L.Cailleux / Location = DGA/MI (Bruz) or Telecom Bretagne (Rennes)
  83. Categorical Semantics of Distributed Version Control Systems
    Samuel Mimram (LIX, École Polytechnique)
    1-20, 2.2
  84. Categorical Semantics of Distributed Version Control Systems
    Samuel Mimram (LIX, École Polytechnique)
    1-20, 2.2
  85. Categorical Semantics of Distributed Version Control Systems
    Samuel Mimram (LIX, École Polytechnique)
    1-20, 2.2
  86. Enabling clusters with Dynamic Distributed Systems
    Franck Petit, Swan Dubois, UPMC/Inria
    2.18.1
  87. Validation of distributed protocols for opportunistic networks
    Franck Petit, Swan Dubois, UPMC/Inria
    2.18.1
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA