===== Internships 2014/2015 =====

Submit an internship offer

  1. Les représentations équivalentes d'un LFSR filtré et leur impact en cryptanalyse
    Anne Canteaut - Inria Rocquencourt
    2.13.2 et 2.12.1
  2. Analysis of the Mifare Plus Distance Bounding Protocol
    Gildas Avoine, IRISA Rennes
  3. Can SSD Memory Improve Cryptanalytic Time-Memory Trade-O ff?
    Gildas Avoine, IRISA Rennes
  4. Practical Cryptanalysis of Pseudo-Random Number Generators in RFID
    Gildas Avoine
  5. Behaviours as solutions for higher-order programs and processes
    Daniel Hirschkoff, ENS Lyon
    2.3 (2.2)
  6. 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)
  7. Vehicle Sharing Systems: Analysis, modeling, simulation, optimization
    Nicolas GAST - INRIA Monbonnot and Vincent JOST - CNRS G-SCOP Grenoble
  8. Evaluation efficace de polynômes sur les corps finis et application aux implémentations sécurisées contre les attaques par canaux auxiliaires
    Matthieu Rivain, CryptoExperts, Paris
    Cryptography
  9. Types and interpretations for programs of polynomial time complexity
    Patrick Baillot, ENS Lyon
    2.2, 2.1 (2.4)
  10. Résolution symbolique efficace de systèmes d’équations linéaires différentielles et de récurrences
    Frédéric Chyzak et Alin Bostan
  11. Calcul efficace de coefficients de séries
    Frédéric Chyzak et Alin Bostan - INRIA Saclay ÎDF (à Palaiseau)
  12. Preuves algorithmiques pour la transcendance des séries
    Frédéric Chyzak et Alin Bostan - INRIA Saclay ÎDF (à Palaiseau)
  13. 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
  14. Relativized Implicit Computational Complexity and Declassification
    Frédéric Prost - LIP ENS-Lyon
    2.1 / 2.6 /
  15. Translation methods for deciding separation logics
    Stéphane Demri – LSV, ENS Cachan
    2.5.1, 2.9.1, 2.9.2, 2.36.1
  16. www.prism.uvsq.fr/~ystr/stage.html
    Laboratoire PRiSM, Université de Versaille Saint QUentin
    Techniques de théorie des jeux en informatique
  17. 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
  18. É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
  19. 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
  20. Modèles mécaniques formels pour l'algorithmique distribuée (essaims de robots)
    Xavier Urbain, LRI (PCRI, Orsay)
    2.7.2
  21. Modèles mécaniques formels pour l'algorithmique distribuée (comportements probabilistes)
    Xavier Urbain, LRI (PCRI, Orsay)
    2.7
  22. Synchronization and Concurrency in Software-Defined Networking
    Petr Kuznetsov, ENST
    2.3
  23. Highly Concurrent Data Structures
    Petr Kuznetsov, ENST
    2.3
  24. Mathematics for Efficient and Robust Distributed Computing
    Petr Kuznetsov, ENST
    2.3
  25. Arrangements of DP-ribbons
    Michel Pocchiola (Paris 6) & Vincent Pilaud (École Polytechnique)
    2-38-1
  26. Multitriangulations de surfaces
    Vincent Pilaud (École Polytechnique)
    2-38-1
  27. Graphes plongés sur les surfaces: algorithmes pour la génération et le plongement
    Luca Castelli Aleardi (Ecole Polytechnique)
    2-38-1
  28. 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
  29. Distributed Algorithms Run By Selfish Agents
    Pierre Fraigniaud and Paolo Penna, LIAFA, Univ. Paris Diderot
    2.18.1
  30. Exploring the Limits of Distributed Computation: Local Graph Coloring
    Pierre Fraigniaud and Adrian Kosowski, LIAFA, Univ. Paris Diderot
    2.18.1
  31. Decision procedures for FOLTL
    Julien Brunel - ONERA - Toulouse
  32. Temporal multi-agent logic for requirement modelling
    Julien Brunel - ONERA - Toulouse
  33. Réseaux sociaux: outils géométriques et combinatoires pour l'analyse et visualisation des réseaux complexes
    Luca Castelli Aleardi et Maks Ovsjanikov (Ecole Polytechnique)
    2-38-1
  34. 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
  35. 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
  36. 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
  37. Verifying replicated data structures: causal consistency
    Ahmed Bouajjani and Constantin Enea - LIAFA, Univ. Paris Diderot
    2.3 - 2.9.2 - 2.18.2
  38. 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
  39. A distributed log for scalable big-data storage
    Alejandro Tomsic, IP6 (Paris)
  40. Version management for big-data storage
    Marc Shapiro, LIP6 (Paris)
  41. Coinductive and symbolic algorithms for non standard automata
    Damien Pous, LIP, ENS Lyon
  42. Formalisation and certification of ownership in a specialised Java virtual machine
    Damien Pous, LIP, ENS Lyon
  43. PiCoq: pi-calculus within Coq
    Damien Pous, LIP, ENS Lyon
  44. Evaluation et amélioration de la sécurité des implémentations de cryptographie symétrique
    Julien Bringer - Morpho - Osny
    2.12 2.13 2.30
  45. Calcul sécurisé efficace et sûr
    Julien Bringer - Morpho - Issy-Les-Moulineaux
    2.12 2.13 2.30
  46. Calcul vérifiable pour la biométrie
    Julien Bringer - Morpho - Issy-Les-Moulineaux
    2.12 2.13 2.30
  47. 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
  48. QtShanoir, un service web pour l’interopérabilité entre systèmes de gestion et de traitement des données en imagerie médicale
    Justine Guillaumont - Rennes
  49. From Completeness to Normalization
    Olivier Hermant (Mines and Inria Paris)
    2.7.1 (Foundations of Proof Systems) and 2.7.2 (Proof Assistants)
  50. Compilation certifiée de réseaux de Petri colorés
    Frédéric Gava (LACL) et Franck Pommereau (IBISC)
  51. Implantation distribué de modèles concurrents
    Frédéric Gava (LACL) et Franck Pommereau (IBISC)
  52. Vérification d'algorithmes de Model checking
    Frédéric Gava et Julien Tesson (LACL)
  53. 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
  54. Erreurs d'arrondi en analyse numérique
    Sylvie Boldo - Inria Saclay
    2.7.2 2.36.1
  55. Querying Probabilitistic Data via Tree Decompositions
    Pierre Senellart - Télécom ParisTech & National University of Singapore
    2.26.2, 2.26.1, 2.16
  56. Canonical form of Boolean network & properties
    Franck Delaplace - IBISC LAB, Tarek Melliti - IBISC LAB
    I32,
  57. 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)
  58. inSitu Topology: Visualisation pour le Calcul Haute Performance
    Julien Tierny _julien.tierny@lip6.fr_, Sorbonne Universites UPMC - LIP6, Paris (Metro 7, 10)
  59. 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
  60. Sémantique formelle des proxies de la prochaine version de JavaScript
    Alan Schmitt - Inria Rennes
    2.7.2, 2.36.1
  61. Proof of convergence for a spacecraft guidance rendezvous algorithm
    M. Joldes, C. Louembet - LAAS-CNRS, Toulouse
  62. Interactions entre profilage statique et ordonnancement
    Florian Brandner, ENSTA
  63. É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
  64. Data intensive management systems concurrency control Coq mechanization
    V. Benzaken, É. Contejean, LRI - CNRS Orsay
  65. É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
  66. Define an internalization of Homotopy Type Theory in Coq
    N. Tabareau/M. Sozeau - Inria, Nantes-Paris
    2.7.2
  67. Define and implement a general notion of higher inductive types
    N. Tabareau/M. Sozeau - Inria, Nantes-Paris
    2.7.2
  68. Parallel algorithms for geometric information analysis from 3D scanners
    Sylvain Contassot-Vivier and Adrien Krähenbühl - LORIA Nancy
  69. Proof-Theoretic Strengh of MSO on Infinite Words
    Colin Riba – LIP - ENS de Lyon
    2.16, 2.20.2
  70. 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
  71. É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
  72. Information per time unit in timed systems
    E. Asarin and A. Degorre - LIAFA
    2-8-2
  73. Compression of mixed (discrete-continuous) signals
    E. Asarin and A. Degorre - LIAFA
    2-8-2
  74. Nouvelles abstractions logicielles pour les réseaux optiques SDN
    Cédric Ware - Télécom ParisTech
  75. Optimal mechanisms for the protection of confidential information
    Catuscia Palamidessi and Konstantinos Chatzikokolakis. INRIA and Ecole Polytechnique
  76. Topology of singular curves and surfaces
    Guillaume Moroz et Marc Pouget
    ALGO COCA 2.22 2.13.1
  77. Standardisation in the linear substitution calculus
    Delia Kesner - PPS - Univ. Paris-Diderot
  78. A New Operational Semantics for the Focalized Intuitionistic Sequent Calculus
    Delia Kesner - PPS - Univ. Paris-Diderot
  79. Analyse de la sécurité d'algorithmes de chiffrement authentifié
    Thomas Fuhr et Henri Gilbert - ANSSI, Paris
  80. Verified JIT compilation of Coq
    Xavier Leroy, Maxime Dénès – Inria Paris-Rocquencourt
    2-4, 2-7-1, 2-7-2
  81. Vérification formelle d’analyses de complexité
    Francois Pottier et Arthur Charguéraud, INRIA Paris-Rocquencourt
    2.4, 2.7.2, 2.36.1
  82. A game-theoretic approach to controller synthesis for the acrobot swing-up problem
    Nicolas Perrin - Paris
    2.8.2, 2.20.1, 1-19, 1-22
  83. Conception et implémentation d’un outil et d’une librairie OCaml pour manipuler les lieurs
    Francois Pottier, INRIA Paris-Rocquencourt
    2.4
  84. Games of imperfect information over graphs
    Patricia Bouyer (LSV), Samson Lasaulce (L2S), Nicolas Markey (LSV)
    2.20.1, 1.22, 1.24
  85. 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
  86. 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é
  87. Static analysis by abstract interpretation of the functional correctness of vector and matrix manipulating programs
    Antoine Miné - École normale supérieure
    2.6
  88. Analyse fonctionnelle en Coq
    Sylvie Boldo - Inria Saclay
    2.7.2
  89. Analyse des erreurs d'arrondi d'une bibliothèque d'analyse numérique
    Sylvie Boldo - Inria Saclay
    2.36.1
  90. Algorithmic issues in MapReduce
    E. Bampis, G. Lucarelli, D. Trystram - INRIA Grenoble or LIP6
    2.24.1, 2.29.1
  91. 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
  92. Comparison of robustness and samplability for timed automata
    Pierre-Alain Reynier (LIF)
    2.8.2
  93. Deciding rational functions among regular ones using streaming string transducers
    Pierre-Alain Reynier (LIF)
    2.16
  94. Programing of an image description API
    Vincent Delaitre
  95. Approximation Algorithms for Combinatorial Optimization Problems in Geometry
    Nabil Mustafa - LIGM Universite Paris-Est
  96. 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
  97. Evolutionary Algorithm: Mixture-Model Extension of CMA-ES for Multi-Modal Optimization
    François Fages - Inria Paris-Rocquencourt
    2.24.1, 2.19
  98. Tropical constraint methods for reducing biochemical reaction systems with multiple timescales
    François Fages - Inria Paris-Rocquencourt
    2.19, 2.13.1
  99. Boucles de rétroaction positive et multistationarité dans des systèmes de réactions biochimiques
    Sylvain Soliman - Inria Paris-Rocquencourt
    C2.19, C2.29.1
  100. 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
  101. Approximation Algorithms for Combinatorial Optimization Problems in Geometry
    Nabil Mustafa - LIGM Universite Paris-Est
  102. Boolean models of biochemical reactions
    François Fages - Inria Paris-Rocquencourt
    C2-19, C2.6
  103. Proof Engineering Tools for Coq
    Eelco Visser and Pierre Neron and Andrew Tolmach - TU Delft - Netherlands)
    2.7.2 2.4
  104. Accurate and Efficient Disjunctions of Abstract Properties of Memory States
    Xavier Rival - DIENS
    2.6
  105. Abstraction de Relations entre États de la Mémoire
    Xavier Rival - DIENS
    2.6
  106. Formal Study of a Countermeasure Against Side-Channel Attacks
    Pablo Rauzy and Sylvain Guilley, at Télécom ParisTech
  107. Protecting Elliptic Curve Cryptography Against Fault Injection Attacks
    Pablo Rauzy and Sylvain Guilley, at Télécom ParisTech
  108. Formalizing Functions as Processes
    Beniamino Accattoli - INRIA Saclay, Parsifal Team
  109. 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
  110. Approximate model reduction for the differential semantics of rule-based models
    J Feret, DI - Ecole normale supérieure, 75005 Paris
    M2 - 6: Abstract interpretation
  111. 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
  112. Functional Programming and Operating System research
    Thomas Gazagnaire - University of Cambridge
  113. Gelfand duality for compact partially ordered spaces
    Emmanuel Haucourt - École Polytechnique (LIX)
    Concurrency 2.3
  114. almost free categories
    Emmanuel Haucourt - École Polytechnique (LIX)
    Concurrency 2.3
  115. Sémantique opérationnelle catégorique
    Tom Hirschowitz - Chambéry
    1-20;2.2;2.3
  116. Strong normalisation for simply typed lambda-calculus: a quest for new combinatorial proofs
    Stefano Guerrini, Giulio Manzonetto
    2.1, 2.2 et 2.4
  117. Résolution de contraintes pour la vérification de programmes
    Sébastien Bardin, CEA LIST (Paris-Saclay)
  118. Génération de tests structurels pour des critères avancés
    Sébastien Bardin, Nikolay Kosmatov, CEA
  119. Réalisation d'outils pour le décodage d'exécutables
    Sébastien Bardin, CEA LIST (Paris-Saclay)
  120. Génération automatique d'exploits à partir de traces d'erreurs
    Marie-Laure Potet, Laurent Mounier (Verimag), Sébastien Bardin (CEA)
  121. Negotiation of correspondence policies
    A.Bouabdallah - L.Cailleux / Location = DGA/MI (Bruz) or Telecom Bretagne (Rennes)
  122. Categorical Semantics of Distributed Version Control Systems
    Samuel Mimram (LIX, École Polytechnique)
    1-20, 2.2
  123. Categorical Semantics of Distributed Version Control Systems
    Samuel Mimram (LIX, École Polytechnique)
    1-20, 2.2
  124. Categorical Semantics of Distributed Version Control Systems
    Samuel Mimram (LIX, École Polytechnique)
    1-20, 2.2
  125. Enabling clusters with Dynamic Distributed Systems
    Franck Petit, Swan Dubois, UPMC/Inria
    2.18.1
  126. Validation of distributed protocols for opportunistic networks
    Franck Petit, Swan Dubois, UPMC/Inria
    2.18.1