Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Internships 2015/2016

  1. Test
    tester
    test
  2. F*: From Program Verification System to Proof Assistant
    Catalin Hritcu - Inria Paris
    2.4, 2.36.1, 2.7.2, 2.7.1, 2.5.1, 1.20, 2.1, 2.6
  3. Generating Counterexamples for Coq and TLA+ Proof System
    Jasmin Blanchette and Simon Cruanes - Inria Nancy ou Max-Planck-Institut für Informatik Saarbrücken
  4. Alarm prediction via space-time pattern matching
    Anne Bouillard, Philippe Jacquet or Marc-Olivier Buob, LINCS
  5. Contrôle dans les réseaux
    Anne Bouillard, Nadir Farhi
  6. Irréductibilité computationnelle et ASM
    Julien Cervelle et Pierre Valarcher (LACL, Université Paris Est Créteil)
  7. QuickChick: Property-Based Testing for Coq
    Catalin Hritcu - Inria Paris
    2.4, 2.36.1, 2.7.2, 2.5.1, 1-31, 1-20
  8. Highly Concurrent Data Structures
    Petr Kuznetsov (Telecom ParisTech/EPFL)
    2.18.2/2.3
  9. Synchronization in Distributed SDN Control Planes
    Petr Kuznetsov (Telecom ParisTech)
    2.18.2/2.3
  10. Proofs of preprocessing in Satisfiability Modulo Theories
    Pascal Fontaine and Jasmin Blanchette - Loria, Inria Nancy
  11. Graph polynomials and combinatorial Hopf algebras
    Adrian Tanasa and Jean-Christophe Aval - Labri (Bordeaux)
    2.38.1, 2.10
  12. Computational complexity of Graph Data Exchange
    Angela Bonifati (Liris, Univ. Lyon 1)
  13. Noeuds et sphères collapsables
    Luca Castelli Aleardi et Thomas Lewiner (LIX, Ecole Polytechnique)
    2.38.1, 2.10
  14. Bijective analysis of greedy online algorithms
    Spyros Angelopoulos–LIP6/UPMC
  15. Algorithms for expanding search
    Spyros Angelopoulos–LIP6/UPMC
  16. Analyse fonctionnelle en Coq
    Sylvie Boldo - Orsay
    2.7.2
  17. Erreurs d'arrondi en analyse numérique
    Sylvie Boldo - Orsay
    2.7.2 2.36.1
  18. Superposition et superdéduction en théorie des ensembles
    Guillaume Burel, Simon Cruanes, et David Delahaye - Inria Saclay (ENS Cachan)
    2.4, 2.5.1, 2.7.1, 2.7.2, 2.36.1
  19. Analyse topologique de circuits électroniques
    L. Fribourg, E. Goubault, S. Putot
    2.5.1, 2.6, 2.7, 2.8.2, 2.9
  20. Relation algebra without complement
    Damien Pous - LIP, ENS Lyon
    1-18, 1-22, 1-33, 2.7.1, 2.7.2
  21. Coinductive and symbolic algorithms for challenging automata models
    Damien Pous - LIP, ENS Lyon
    1-18, 1-22, 2.16, 2.20.2, 2.9.2, 2.15, 2.7.1, 2.7.2
  22. Verified JIT compilation of Coq
    Xavier Leroy - Inria Paris
    2-4, 2-7-1, 2-7-2
  23. Plongements topologiques de graphes dans des 2-complexes simpliciaux
    Éric Colin de Verdière - ENS, Paris 5ème
    2-38-1, 2-29-1
  24. Décroisements de graphes dans le plan avec obstacles
    Éric Colin de Verdière - ENS, Paris 5ème
    2-38-1, 2-29-1
  25. Linear graph rewriting for Boolean logic
    Olivier Laurent, Anupam Das - LIP, ENS Lyon
    2.29.1 , 1-33 , 2.1
  26. Application du calcul sécurisé au machine learning
    Constance Morel, Morpho, Issy-Les-Moulineaux
    2.12.1, 2.12.2
  27. Application de primitives de chiffrement efficaces pour la recherche de données
    Roch Lescuyer, Morpho, Issy-Les-Moulineaux
    2.12.1, 2.12.2
  28. Application du chiffrement homomorphique à la biométrie
    Constance Morel, Morpho, Issy-Les-Moulineaux
    2.12.1, 2.12.2
  29. Preuve formelle pour les essaims de robots (espaces discrets)
    X. Urbain, P. Courtieu, S. Tixeuil - LRI, Orsay
    2.7.2, (2.18.1)
  30. Quantitative Types for Classical Logic
    Delia Kesner - PPS, Univ. Paris-Diderot
  31. Recherche textuelle
    Orchestra Networks - Paris
  32. Modèles de données temporels
    Orchestra Networks - Paris
  33. Relativistic Cryptography
    André Chailloux - Inria Paris
    2.34.1
  34. Quantum Simulation
    André Chailloux - Inria Paris
    2.34.1
  35. Arrangements of DP-ribbons
    Michel Pocchiola (Paris 6) & Vincent Pilaud (École Polytechnique)
    2-38-1
  36. Le diamètre du multiassociaèdre
    Lionel Pournin (Paris 13) & Vincent Pilaud (École Polytechnique)
    2-38-1, 2-10
  37. Coq formalisation and mechanisation of privacy aware data integration
    Thibaut Balabonski Véronique Benzaken Évelyne Contejean (LRI - U. Paris Sud)
  38. A Parallel Synchronous Language for Computational Control Systems
    Albert Cohen, Marc Pouzet - ENS Paris
    2.23.1, 2.37.1
  39. Étude du contrôle adaptatif de processus dynamiques dans les systèmes multimédia interactifs
    Dimitri Bouche, Jean-Louis Giavitto - Ircam, 1 place Igor-Stravinsky, 75004 Paris
  40. Machine-verified Code Generation for a Lustre Compiler
    Tim Bourke, Marc Pouzet, ENS Paris
    2.23.1, 2.7.2
  41. Concurrent Program Synthesis
    Azadeh Farzan - University of Toronto - Toronto, Canada
    http://www.cs.toronto.edu/~azadeh
  42. The Strength of Safra’s Construction
    Colin Riba - LIP, ENS de Lyon or Henryk Michalewski - MIMUW, Univ. Warsaw
    2-20-1, 2-20-2
  43. Witness Extraction for MSO on Infinite Words
    Colin Riba - LIP, ENS de Lyon or Henryk Michalewski - MIMUW, Univ. Warsaw
    2-20-1, 2-20-2, 2-7-1, 2-7-2
  44. Codes stencils et calculs hautes performances
    Sid Touati, Albert Cohen - INRIA Sophia Antipolis
    2.37.1
  45. Formal specification and model checking of requirement models
    J. Brunel & D. Chemouil - Onera/DTIM, Toulouse
  46. Practical Interpolation on Partially Ordered Datasets
    Antoine Amarilli & Pierre Senellart, Télécom ParisTech
    2.11, 2.26.1, 2.26.2
  47. Quantitative Partial Order Representations of Preference Data
    Antoine Amarilli & Pierre Senellart, Télécom ParisTech
    2.26.1, 2.26.2
  48. Query Answering for Expressive Frontier-One Constraints
    Antoine Amarilli & Pierre Senellart, Télécom ParisTech
    2.26.1, 2.26.2
  49. Implémentation et transformations de modèles Altarica 3.0
    Michel BATTEUX - IRT SystemX (Palaiseau)
  50. Redescription de représentation en robotique
    Stéphane Doncieux & Nicolas Perrin - CNRS ISIR (UPMC), Paris
  51. Efficient Formally Secure Compilers to a Tagged Architecture
    Catalin Hritcu - Inria Paris
    2.4, 2.36.1, 2.7.2
  52. Orienting triangulations of genus g≥2
    Daniel Gonçalves - LIRMM (Montpellier)
    2.38.1 Algorithmique et combinatoire des graphes géométriques
  53. A Verified Browser Security Engine
    Karthikeyan Bhargavan - INRIA
    2.30, 2.4, 2.7.1
  54. Attacking and Proving TLS 1.3 implementations
    Karthikeyan Bhargavan - INRIA
    2.30, 2.4, 2.12.1,
  55. Geometric properties of combinatorial systems
    Xavier Goaoc (Univ. Paris Est) and Nabil Mustafa (ESIEE) - Laboratoire d'informatique Gaspard Monge
    2.38.1
  56. Sparse inclusion-exclusion formulas for set systems of bounded VC dimension
    Xavier Goaoc (Univ. Paris Est) and Nabil Mustafa (ESIEE) - Laboratoire d'informatique Gaspard Monge
    2.38.1
  57. Implantation distribu´ee de mod`eles concurrents
    Frédéric Gava (LACL, Paris-Est) et Franck Pommereau (IBISC, Evry)
  58. Vérification d’algorithmes de model-checking
    Frédéric Gava et Julien Tesson (LACL, Paris-Est)
    2.7.2, 2.5.1, 2.9.2, 2.36.1
  59. Compilation certifiée (avec optimisations) en ML/Java/C de réseaux de Petri colorés
    Frédéric Gava (LACL, Paris-Est) et Franck Pommereau (IBISC, Evry) et Julien Tesson (LACL
    2.7.2, 2.5.1, 2.9.2, 2.36.1
  60. Preuves en Coq de programmes multi-ML
    Frédéric Gava et Julien Tesson (LACL, Paris-Est)
    2.4, 2.7.2, 2.36.1, 2.37.1, 2.18.2
  61. From Viper to Grasshopper (and back again)
    Peter Müller, ETH Zurich
    2.3.1, 2.36.1
  62. Towards the Verification of Shell Scripts
    Mihaela Sighireanu and Ralf Treinen - IRIF, Université Paris-Diderot
    2.36.1
  63. Classification des 2-complexes
    Francis Lazarus et Arnaud de Mesmay - Gipsa-Lab, Grenoble
    2.38.1
  64. Call-by-value and call-by-name calculi: syntax, semantics, and logics
    Stefano Guerrini, Giulio Manzonetto - LIPN Paris 13
    2.1, 2.2
  65. Strong normalisation for simply typed lamba-calculus: a quest for new combinatorial proofs
    Stefano Guerrini, Giulio Manzonetto - LIPN Paris 13
    2.1,2.2
  66. Implémentation instrumentable du protocole IKEv2
    Pierre Néron - ANSSI Paris
    2-30, 2-4
  67. Vérification structurelle d'applications JavaCard
    Pierre Néron - ANSSI Paris
    2-7-2, 2-36-1
  68. Synthesis of Concurrent Implementations from Sequential Ones
    Ahmed Bouajjani, IRIF (LIAFA), Univ Paris Diderot, Bat Sophie Germain, Paris 13eme.
  69. Etude et implantation d’une méthode algébrique pour résoudre des systèmes à coefficients flous
    Philippe Aubry, Annick Valibouze - LIP6, Université Paris 6 (UPMC)
  70. Model Checking on the fly for ATL*
    Serenella Cerrito-Ibisc (Evry)
  71. Information per time unit in timed systems
    E. Asarin and A. Degorre - IRIF
    2-8-2
  72. Compression of mixed (discrete-continuous) signals
    E. Asarin and A. Degorre - IRIF
    2-8-2
  73. Trier sur un cycle
    Christoph Dürr - LIP6
    2-24-[12]
  74. Formalizing Abstract Machines
    Beniamino Accattoli - INRIA Saclay, Parsifal team
  75. Protection of private information
    Catuscia Palamidessi and Kostas Chatzikokolakis – INRIA and Ecole Polytechnique
    2.3.2: Foundations of privacy
  76. Nids de serpents et arrangements de tuyaux
    Vincent Pilaud et Thibault Manneville - École Polytechnique
    2-38-1, 2-10
  77. Influence vs Reaction Systems
    François Fages
    2-19, 2-6,
  78. Biochemical Program Compiler
    François Fages
    2-19,
  79. Performance study of making IDSs self-adaptable in IaaS clouds
    Christine Morin, Louis Rilling - IRISA / Inria Rennes
  80. Formules d'inclusion-exclusion et algorithmique des graphes
    Xavier Goaoc et Éric Colin de Verdière - ENS Paris ou U. Marne la Vallée
    2-29-1,2-10,2-38-1
  81. Transducteurs bidirectionnels en entrée et en sortie
    Olivier Carton & Olivier Serre (LIAFA)
  82. Games with Hierarchical Objectives
    Ocan Sankur - Irisa, Rennes
    1.22, 2.8, 2.9
  83. Lagrangian Duality in Online Algorithms
    Christoph Dürr and Nguyen Kim Thang, University Paris 6 and University Evry
  84. New Quantum Algorithms for k-Clique
    Frederic Magniez - IRIF (ex PPS-LIAFA), U. Paris Diderot
    2.34.1
  85. Composantes connexes d'un nœud dans un flot de liens
    Binh-Minh Bui-Xuan et Clémence Magnien, LIP6, UPMC, Paris.
  86. Scheduling in the clouds
    Luciana Arantes (LIP6), Evripidis Bampis (LIP6) and Giorgio Lucarelli (LIG/INRIA) - internship location: LIP6, UPMC
    2.24.1, 2.24.2
  87. Caract ́erisation de formes : Invariants par rotation des formes quartiques
    Evelyne Hubert & Théo Papadopoulo, Inria Sophia Antipolis
    2.13.1; 2.22
  88. Geometric Analysis of Uncertain Scalar Fields
    Pooran Memari, CNRS-LTICI, Telecom ParisTech; Julien Tierny, CNRS-LIP6, UPMC.
    2.14.1 (S) Analyse géométrique des données Computational geometry learning
  89. Algorithms for Global Illumination
    Venceslas Biri (UPEM, Universite Paris-Est) and Nabil Mustafa (ESIEE, Universite Paris-Est)
  90. Trier sur un cycle
    Christophe Durr - P6
    2.24.2
  91. Root solver using subdivision and Fast Fourier Transform
    Guillaume Moroz, Marc Pouget, Rémi Imbach
    2.22 2.13.1
  92. Homomorphic encryption beyond semantic security
    Fabien Laguillaumie and Benoît Libert - ENS de Lyon
 
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