Internships 2016/2017

  1. Quantum Walking in a Discrete Geometry
    Pablo Arrighi, Giuseppe Di Molfetta - LIF, Luminy
    2.34.1
  2. Analog continuous time machines and models of computation
    Olivier Bournez, Ecole Polytechnique, LIX, Palaiseau
  3. Temporal logics on strings
    Stéphane Demri – LSV, Cachan
    1.22, 2.5.1, 2.9.1
  4. VASS games for resource-bounded logics
    Stéphane Demri – LSV, Cachan
    1.22, 2.5.1, 2.9.1, 2.20.1
  5. Decision procedures for separation logics
    Stéphane Demri – LSV, Cachan
    2.5.1, 2.9.1, 2.9.2, 2.36.1
  6. Formally Secure Compilation
    Catalin Hritcu - Inria Paris
    2.4, 2.36.1, 2.7.2, 2.30
  7. Contraintes sur des domaines paramétriques
    Charlotte Truchet - Nantes
    2.6, 2.35.1
  8. Grph polynomials
    JC Aval & A. Tanasa, LABRI
    Combinatorics
  9. M´ethode GLV en dimension 4 sur les Q-courbes
    Olivier Bernard, Renaud Dubois, Olivier Orcière - THALES COMMUNICATIONS
  10. Attaques par canaux auxiliaires sur les schémas post-quantiques
    Ange Martinelli, Thomas Prest - THALES COMMUNICATIONS
  11. Sécurisation du Cloud – Schémas de recherche sur données chiffrées avancées
    Alexandre Anzala Yamajako
  12. Sécurisation du Cloud – Schémas de recherche sur données chiffrées avancées
    Alexandre Anzala Yamajako, Emeline Hufschmitt
  13. Graphes plongés sur les surfaces: algorithmes pour la génération et le plongement en genre supérieur
    Luca Castelli Aleardi - Eric Fusy (LIX, Polytechnique)
    http://www.lix.polytechnique.fr/~amturing/stages.html#StageGenerationGenreSuperieur
  14. Separation Logic-based Abstraction, Three Valued Logic Abstraction and Reduction
    Xavier Rival (ENS Paris / INRIA)
    2.6
  15. Separation Logic with Summary Predicates Described by Set Universal Quantification
    Xavier Rival (ENS Paris / INRIA)
  16. Robust methodology for the comparison of clinical metagenomic samles
    Macha Nikolski - Bordeaux
  17. Bayesian update as fixed-point transformation
    Kostas Chatzikokolakis and Catuscia Palamidessi
    2.3.2
  18. Information per time unit in timed systems
    E.Asarin & A.Degorre- IRIF, Paris
    2.8.2,2.9.1,2.9.2,2.10,2.22
  19. Compression of mixed (discrete-continuous) signals
    E.Asarin & A.Degorre- IRIF, Paris
    2-8-2
  20. Protocoles d'échange de clefs à base d'isogénies
    Luca De Feo, François Morain (Inria Saclay), Jean-Pierre Flori, Jérôme Plût (ANSSI)
    2.12.1, 2.12.2, 2.13.1, 2.13.2
  21. Comparison of approaches to quantitative verification
    E. Asarin and A. Degorre - IRIF
    2.8.*,2.9.*
  22. Reversible Causal Graph Dynamics : emergence
    Pablo Arrighi, Simon Martiel - LIF, Luminy / IXXI, Lyon
  23. Linux Packages and Tree Transducers
    Sylvain Salvati, Aurélien Lemay
  24. Combining dimensionality reduction and feature detection, with applications to molecular data analysis
    Frederic Cazals; Inria Sophia Antipolis
  25. Experimental cryptanalysis of the DES – how far can we go?
    Pr. François-Xavier Standaert - UCL (Belgium)
  26. Side-channel measurements simulator and formal methods
    Pr. François-Xavier Standaert - UCL (Belgium)
  27. Deep Reinforcement Learning Techniques for 5G Networks Optimization
    Stephane Senecal - Orange Labs
  28. Vérification formelle performante pour la logique temporelle relationnelle sur domaines borné
    J. Brunel & D. Chemouil, ONERA Toulouse
    2-5, 2-20-2
  29. Efficacité et stabilité en optimisation dynamique
    Evripidis Bampis et Bruno Escoffier
    2.24.1 2.24.2 2.29.1
  30. Efficient Homomorphic Encryption and Applications
    Malika Izabachène - Nicolas Gama - CEA, LIST
  31. Le diamètre des multiassociaèdres et des accordéoèdres
    Vincent Pilaud (École Polytechnique) & Lionel Pournin (Université Paris 13)
    2-38-1, 2-10
  32. Calcul vérifiable pour Coq
    Chantal Keller (LRI, Orsay)
  33. Utilisation de prouveurs automatiques en Coq
    Chantal Keller (LRI, Orsay)
  34. Segmentation semi-automatique de champs volumiques bivariés par surfaces fibrées
    Julien Tierny - LIP6
  35. Verification of security protocols: decidability results
    Stéphanie Delaune (Rennes), Véronique Cortier (Nancy)
    2.30
  36. Contrôle topologique d'évolutions d'objets géométriques
    S. Alayrangues, P. Lienhardt, S. Peltier - Poitiers (XLIM, UMR CNRS 7252, Université de Poitiers)
    algorithmique et combinatoire des graphes géométriques
  37. Preuves en Coq de Programmes Multi-ML
    Frédéric Gava
    http://lacl.univ-paris12.fr/gava/stages/CoqMulti.pdf
  38. Conception d'algorithmes multi-BSP sur les graphes et leur implantation à l'aide d'une extension de OCaml dédiée à la programmation distribuée multi-BSP
    Frédéric Gava
  39. Intersurf++
    Dave Ritchie- Nancy
  40. Algorithme de calcul d'isogénies de Lercier et Sirvent
    Jean-Pierre Flori, Jérôme Plût (ANSSI, prénom.nom@ssi.gouv.fr), Luca De Feo, François Morain (Inria Saclay)
    2.12.1, 2.12.2, 2.13.1, 2.13.2
  41. Computational Algebra in Rust-
    Morten Dahl, Snips (snips.ai)
    2.22, 2.12.2, 2.13.1, 2.13.2
  42. Specialised Zero-Knowledge Proofs
    Morten Dahl, Snips (snips.ai)
    2.12.1
  43. Homomorphic Encryption
    Morten Dahl, Snips (snips.ai)
    2.12.1, 2.13.1
  44. Private Data Analysis
    Morten Dahl, Snips (snips.ai)
    2.3.2
  45. Gestion d’erreurs de modèles AltaRica 3.0
    M. Batteux - IRT SystemX (Palaiseau)
  46. Visualisation de modèles AltaRica 3.0
    M. Batteux - IRT SystemX (Palaiseau)
  47. Comportements génériques de modèles AltaRica 3.0
    M. Batteux - IRT SystemX (Palaiseau)
  48. Contrôle d’accès dans les bases de données : conception et vérification
    Pierre Bourhis et Sophie Tison
    https://www.cristal.univ-lille.fr/~tison/ProjetMasterBourhisTison.pdf
  49. Support for the Rust language in AdaCore's suite of tools
    Raphael Amiard
    2.37.1
  50. Formally prove control ow graph algorithms in SPARK
    Claire Dross
    2.5.1 (S), 2.36.1
  51. Light-weight static analysis of critical embedded code
    Yannick Moy
    2.6
  52. Persistence-based reconstruction
    Marc Glisse - Inria Saclay Palaiseau
    2.14.1
  53. Verifying replicated data structures: causal consistency
    Constantin Enea - IRIF, University Paris Diderot
    2.6, 2.8.1, 2.9.2, 2.18.1, 2.18.2, 2.26.2
  54. Vector-Dijkstra
    Mathijs Wintraecken and Jean-Daniel Boissonnat INRIA Sophia-Antipolis
    2.14.1
  55. Polynomial geodesic approximation
    Mathijs Wintraecken and Jean-Daniel Boissonnat, INRIA Sophia-Antipolis
    2.14.1
  56. Verification and Synthesis of Concurrent Programs
    University of Toronto, Canada — Azadeh Farzan
  57. Synthèse de contrôle hybride en présence d'information partielle
    Laurent Fribourg - LSV, ENS Cachan
    2.8.2
  58. Provenance-Based Routing in Road and Transport Networks
    Pierre Senellart (ENS Paris) & Silviu Maniu (LRI)
    2.26.2, 2.29.1, 2.29.2
  59. How to Evaluate the Compliance of a Security Event Flow Setup to SLAs
    Christine Morin _christine.morin@inria.fr_, Amir Teshome _amir-teshome.wonjiga@inria.fr_, Louis Rilling _louis.rilling@irisa.fr_ - IRISA / Inria Rennes
    1-34, 1-36, 2.18.1, 2.24.1
  60. Certified and Optimizing Bit Slicing Compiler
    Pierre-Evariste Dagand - LIP6, Paris
  61. Étude du protocole et de l'écosystème SSH
    Olivier Levillain - ANSSI
  62. Characterizing Tractable Queries and Probabilistic Instance Families
    Antoine Amarilli - Télécom ParisTech
  63. Static Analysis by Abstract Interpretation of Core Python Programs
    Antoine Miné (LIP6, UPMC)
    2.6
  64. Sampling Informative Patterns from Large Networks
    Mostafa H. Chehreghani and Albert Bifet and Talel Abdessalem - Telecom ParisTech
    2.29.2
  65. Verifying Lustre to the Binary
    Timothy Bourke and Marc Pouzet (ENS)
    Parallélisme synchrone
  66. Optimiser les jeux sous incertitude
    Florian Richoux - Université de Nantes
  67. Contrôle probabiliste et distribué de la demande pour les réseaux électriques intelligents
    Supervisors: Beaude, Bendottti, Oudjane (EDF R&D) - Busic (Inria / Dép. d'informatique de l'ENS); Location of the internship: EDF R&D campus Saclay
    1-24, 1-30, 2.17.1, 2.18.1
  68. Verification of Security Protocols
    Bruno Blanchet, Harry Halpin - Inria Paris
    2-30
  69. Verification of Security Protocols
    Bruno Blanchet, Harry Halpin - Inria Paris
    2-30
  70. Efficient and modular higher-order rewriting
    Frédéric Blanqui (Cachan) and Christophe Raffalli (Chambéry)
    1-33, 2.7.1, 2.7.2
  71. Termination checking in Dedukti
    Frédéric Blanqui (Cachan)
    1-33, 2.7.1, 2.7.2, 2.4
  72. Proof tactics in Dedukti
    Frédéric Blanqui (Cachan)
    1-33, 2.7.1, 2.7.2, 2.5.1
  73. Interactive proofs with Dedukti
    Frédéric Blanqui (Cachan) and Emilio Gallego (Mines ParisTech)
    1-33, 2.7.1, 2.7.2, 2.4
  74. Refinement in Dedukti
    Frédéric Blanqui (Cachan)
    1-33, 2.7.1, 2.7.2, 2.4
  75. Spectral Graph Theory
    F. Nataf, equipe LJLL-INRIA Alpines
  76. Verifying Robustness of Distributed Systems against Weak Consistency Models.
    Ahmed Bouajjani and Constantin Enea – IRIF, Univ Paris Diderot
  77. Automating Higher-Order Logic
    Jasmin Blanchette & Pascal Fontaine - Nancy (in collaboration with Amsterdam and Saarbrücken)
  78. Building DNA computers: theory and experiments
    Damien Woods, Inria, Paris
  79. Deep specification and verification of a SQL query planner
    Véronique Benzaken, Évelyne Contejean et Chantal Keller (LRI, Orsay)
  80. Symbolic Execution of Shell Scripts
    Mihaela Sighireanu - IRIF, University Paris Diderot
    2.6,2.7.2,2.9.2,2.36.1
  81. Symbolic Execution of Shell Scripts
    Mihaela Sighireanu - IRIF, University Paris Diderot
    2.6,2.7.2,2.9.2,2.36.1
  82. Random walks on hypergraphs
    T. Abdessalem, L. Decreusefond
  83. Reputation and the evolution of cooperation in collective adaptive systems
    Nicolas Bredeche - ISIR
  84. Dynamic matching models
    Ana Busic - Inria Paris
    1-24, 1-30, 2.17.1
  85. Types pour la complexité implicite
    Patrick Baillot - LIP, ENS de Lyon
    2.1, 2.4
  86. Ordonnancement tolérant aux fautes en minimisant la consommation d'énergie dans les environnements répartis
    Luciana Arantes (LIP6/INRIA), Evripidis Bampis (LIP6) et Giorgio Lucarelli (LIG/INRIA), Pierre Sens (LIP6/INRIA)
  87. Superposition modulo en théorie des ensembles
    David Delahaye (LIRMM), Simon Cruanes (Loria)
    1-33, 2.4, 2.5.1 (S), 2.7.1, 2.7.2
  88. Vérification formelle du logiciel HILECOP
    David Andreu (LIRMM), Baptiste Colombani (LIRMM), David Delahaye (LIRMM)
    1-22, 2.4, 2.7.2, 2.8.2, 2.23.1
  89. Utilisation de SMT-solver pour la génération automatique d'algorithmes répartis pour des réseaux de robots collaboratifs
    Nathalie Sznajder - Souheib Baarir
  90. Modèle unifié et algorithmes pour les jeux stochastiques
    Yann Strozecki- Laboratoire David Université de Versailles
  91. Complexité d'énumération : liens avec la génération aléatoire
    Yann Strozecki- Laboratoire David Université de Versailles
  92. Algorithmique de graphes pour la cheminformatique
    Yann Strozecki- Laboratoire David Université de Versailles
  93. Utilisation de SMT-solver pour la génération automatique d'algorithmes répartis pour des réseaux de robots collaboratifs
    Nathalie Sznajder, Souheib Baarir (Lip6)
  94. Combinatoire des polynomes de Koornwinder
    Sylvie Corteel (IRIF, CNRS et Universite Paris Diderot)
    C2-10
  95. Quantitative types for the atomic lambda-calculus
    Delia Kesner - Univ Paris-Diderot
  96. Reconfigurable storage in blockchains
    Petr Kuznetov, Telecom ParisTech
    2.18.1, 2.18.2
  97. Internship / Early design error detection (m/f)
    Louis FABRE louis.fabre@airbus.com - Marignane (BdR)
  98. Internship / Aircraft Secured Connectivity - content filter evaluation (m/f)
    Louis Fabre louis.fabre@airbus.com - Marignane (BdR)
  99. Self-Adjusting Parameter Choices for Discrete Black-Box Optimization
    Carola Doerr, Benjamin Doerr - LIP6 and/or LIX
    2.24.2 Solving Optimization Problems with Search Heuristics
  100. Amélioration d'un Analyseur Statique pour les programmes manipulant des tableaux
    Valentin Perrelle et Matthieu Lemmere. CEA, Nano-Innov, Palaiseau
    2.6
  101. Deep specification and verification of a SQL query planner
    Véronique Benzaken, Évelyne Contejean, Chantal Keller at LRI (Orsay)
  102. Developing the primal dual framework for non-linear combinatorial optimization
    Nguyen Kim Thang (IBISC Evry), et aussi C. Dürr (LIP6)
    2-24-1
  103. Cubical type theory in Dedukti
    LSV
  104. Banach-Mazur Games and Stochastic Games
    Daniele Varacca and Youssouf Oualhadj
  105. The Cost of Continuations
    Beniamino Accattoli - INRIA Saclay
    2.1, 2.2, 2.4, 2.7.1, 2.7.2
  106. Bijective analysis of greedy online algorithms
    Spyros Angelopoulos - LIP6,UPMC
    2:24.1, 2:24.2, 2:29.1