Internships 2015/2016

  1. Test
    tester
    test
  2. Attack-defense trees with dependencies: a security assessment methodology applied to an access control system
    Barbara Kordy and Gildas Avoine - IRISA, Rennes
  3. 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
  4. Automating Data Science with Coq
    Rennes/Nantes
    2.7.2
  5. Generating Counterexamples for Coq and TLA+ Proof System
    Jasmin Blanchette and Simon Cruanes - Inria Nancy ou Max-Planck-Institut für Informatik Saarbrücken
  6. Alarm prediction via space-time pattern matching
    Anne Bouillard, Philippe Jacquet or Marc-Olivier Buob, LINCS
  7. Contrôle dans les réseaux
    Anne Bouillard, Nadir Farhi
  8. Irréductibilité computationnelle et ASM
    Julien Cervelle et Pierre Valarcher (LACL, Université Paris Est Créteil)
  9. Création d’atlas de perfusion cérébrale normale de l’enfant entre 0 et 10 ans
    Olivier Commowick - Inria Rennes, France
  10. Analyse topologique de données 3D pour la visualisation scientifique: clustering topologique
    Julien Tierny - CNRS LIP6 (UPMC), Paris
  11. Analyse topologique de données 3D pour la visualisation scientifique: segmentation de données bivariées
    Julien Tierny - CNRS LIP6 (UPMC), Paris
  12. Analyse topologique de données 3D pour la visualisation scientifique: out-of-core Contour Trees
    Julien Tierny - CNRS LIP6 (UPMC), Paris
  13. 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
  14. Attaques par canaux cachés : implémentations et évaluations pratiques de contre-mesures
    Sonia Belaïd - Thales Genneviliers
    2.12.1, 2.13.2
  15. Verifying replicated data structures: causal consistency
    Constantin Enea - LIAFA
  16. Highly Concurrent Data Structures
    Petr Kuznetsov (Telecom ParisTech/EPFL)
    2.18.2/2.3
  17. Synchronization in Distributed SDN Control Planes
    Petr Kuznetsov (Telecom ParisTech)
    2.18.2/2.3
  18. Joint estimation of neuronal activation and basal metabolism from functional Arterial Spin Labeling
    Rennes
  19. Proofs of preprocessing in Satisfiability Modulo Theories
    Pascal Fontaine and Jasmin Blanchette - Loria, Inria Nancy
  20. On the theory of the probabilistic mu-calculus
    Matteo Mio
  21. On extensions of Monadic Second Order Logic
    Matteo Mio
  22. Graph polynomials and combinatorial Hopf algebras
    Adrian Tanasa and Jean-Christophe Aval - Labri (Bordeaux)
    2.38.1, 2.10
  23. Computational complexity of Graph Data Exchange
    Angela Bonifati (Liris, Univ. Lyon 1)
  24. Graphes plongés sur les surfaces: algorithmes pour la génération et le plongement en genre supérieur
    Luca Castelli Aleardi et Eric Fusy
    2.38.1, 2.10
  25. Noeuds et sphères collapsables
    Luca Castelli Aleardi et Thomas Lewiner (LIX, Ecole Polytechnique)
    2.38.1, 2.10
  26. Bijective analysis of greedy online algorithms
    Spyros Angelopoulos–LIP6/UPMC
  27. Algorithms for expanding search
    Spyros Angelopoulos–LIP6/UPMC
  28. Analyse fonctionnelle en Coq
    Sylvie Boldo - Orsay
    2.7.2
  29. Erreurs d'arrondi en analyse numérique
    Sylvie Boldo - Orsay
    2.7.2 2.36.1
  30. 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
  31. Analyse topologique de circuits électroniques
    L. Fribourg, E. Goubault, S. Putot
    2.5.1, 2.6, 2.7, 2.8.2, 2.9
  32. Relation algebra without complement
    Damien Pous - LIP, ENS Lyon
    1-18, 1-22, 1-33, 2.7.1, 2.7.2
  33. 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
  34. Verified JIT compilation of Coq
    Xavier Leroy - Inria Paris
    2-4, 2-7-1, 2-7-2
  35. Plongements topologiques de graphes dans des 2-complexes simpliciaux
    Éric Colin de Verdière - ENS, Paris 5ème
    2-38-1, 2-29-1
  36. Décroisements de graphes dans le plan avec obstacles
    Éric Colin de Verdière - ENS, Paris 5ème
    2-38-1, 2-29-1
  37. Linear graph rewriting for Boolean logic
    Olivier Laurent, Anupam Das - LIP, ENS Lyon
    2.29.1 , 1-33 , 2.1
  38. Application de la blockchain (bitcoin) à la biométrie H/F
    Roch Lescuyer
    2.12.1, 2.12.2
  39. Application du calcul sécurisé au machine learning
    Constance Morel, Morpho, Issy-Les-Moulineaux
    2.12.1, 2.12.2
  40. Application de primitives de chiffrement efficaces pour la recherche de données
    Roch Lescuyer, Morpho, Issy-Les-Moulineaux
    2.12.1, 2.12.2
  41. Application du chiffrement homomorphique à la biométrie
    Constance Morel, Morpho, Issy-Les-Moulineaux
    2.12.1, 2.12.2
  42. Preuve formelle pour les essaims de robots (comportements probabilistes)
    Xavier Urbain - LRI, Orsay
    2.7.2, (2.11.1)
  43. Preuve formelle pour les essaims de robots (espaces discrets)
    X. Urbain, P. Courtieu, S. Tixeuil - LRI, Orsay
    2.7.2, (2.18.1)
  44. Quantitative Types for Classical Logic
    Delia Kesner - PPS, Univ. Paris-Diderot
  45. Encryption for Fine-Grained Access Control
    Hoeteck Wee
    2.12.1
  46. Comparaison et fusion de données
    Orchestra Networks
  47. Système transactionnel et cache distribué
    Orchestra Networks
  48. Recherche textuelle
    Orchestra Networks - Paris
  49. Modèles de données temporels
    Orchestra Networks - Paris
  50. Types for complexity analysis, with applications to security
    Patrick Baillot
    2.4,2.1,2.12.1,2.30
  51. Relativistic Cryptography
    André Chailloux - Inria Paris
    2.34.1
  52. Quantum Simulation
    André Chailloux - Inria Paris
    2.34.1
  53. Arrangements of DP-ribbons
    Michel Pocchiola (Paris 6) & Vincent Pilaud (École Polytechnique)
    2-38-1
  54. Le diamètre du multiassociaèdre
    Lionel Pournin (Paris 13) & Vincent Pilaud (École Polytechnique)
    2-38-1, 2-10
  55. Coq formalisation and mechanisation of privacy aware data integration
    Thibaut Balabonski Véronique Benzaken Évelyne Contejean (LRI - U. Paris Sud)
  56. A Parallel Synchronous Language for Computational Control Systems
    Albert Cohen, Marc Pouzet - ENS Paris
    2.23.1, 2.37.1
  57. É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
  58. Machine-verified Code Generation for a Lustre Compiler
    Tim Bourke, Marc Pouzet, ENS Paris
    2.23.1, 2.7.2
  59. Concurrent Program Synthesis
    Azadeh Farzan - University of Toronto - Toronto, Canada
    http://www.cs.toronto.edu/~azadeh
  60. The Strength of Safra’s Construction
    Colin Riba - LIP, ENS de Lyon or Henryk Michalewski - MIMUW, Univ. Warsaw
    2-20-1, 2-20-2
  61. 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
  62. Codes stencils et calculs hautes performances
    Sid Touati, Albert Cohen - INRIA Sophia Antipolis
    2.37.1
  63. Formal specification and model checking of requirement models
    J. Brunel & D. Chemouil - Onera/DTIM, Toulouse
  64. Practical Interpolation on Partially Ordered Datasets
    Antoine Amarilli & Pierre Senellart, Télécom ParisTech
    2.11, 2.26.1, 2.26.2
  65. Quantitative Partial Order Representations of Preference Data
    Antoine Amarilli & Pierre Senellart, Télécom ParisTech
    2.26.1, 2.26.2
  66. Query Answering for Expressive Frontier-One Constraints
    Antoine Amarilli & Pierre Senellart, Télécom ParisTech
    2.26.1, 2.26.2
  67. Analyse des relations de causalité pour Z\'elus, un langage synchrone pour les systèmes hybrides
    Timothy Bourke, Marc Pouzet
    2.23.1, 2.4, 2.8.2
  68. Implémentation et transformations de modèles Altarica 3.0
    Michel BATTEUX - IRT SystemX (Palaiseau)
  69. Redescription de représentation en robotique
    Stéphane Doncieux & Nicolas Perrin - CNRS ISIR (UPMC), Paris
  70. Efficient Formally Secure Compilers to a Tagged Architecture
    Catalin Hritcu - Inria Paris
    2.4, 2.36.1, 2.7.2
  71. Orienting triangulations of genus g≥2
    Daniel Gonçalves - LIRMM (Montpellier)
    2.38.1 Algorithmique et combinatoire des graphes géométriques
  72. A Verified Browser Security Engine
    Karthikeyan Bhargavan - INRIA
    2.30, 2.4, 2.7.1
  73. Attacking and Proving TLS 1.3 implementations
    Karthikeyan Bhargavan - INRIA
    2.30, 2.4, 2.12.1,
  74. Geometric properties of combinatorial systems
    Xavier Goaoc (Univ. Paris Est) and Nabil Mustafa (ESIEE) - Laboratoire d'informatique Gaspard Monge
    2.38.1
  75. 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
  76. 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 et Julien Tesson
    2.3.1, 2.4, 2.18.2, 2.29.1, 2.37.1
  77. Implantation distribu´ee de mod`eles concurrents
    Frédéric Gava (LACL, Paris-Est) et Franck Pommereau (IBISC, Evry)
  78. 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
  79. 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
  80. 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
  81. From Viper to Grasshopper (and back again)
    Peter Müller, ETH Zurich
    2.3.1, 2.36.1
  82. Automatic Inference of Quantified Permissions by Abstract Interpretation
    Peter Müller, ETH Zurich
    2.3.1, 2.6, 2.36.1
  83. Termination Analysis of Heap-Manipulating Programs by Abstract Interpretation
    Peter Müller, ETH Zurich
    2.6, 2.36.1
  84. A Formal Semantics for the Viper Intermediate Language
    Peter Müller, ETH Zurich
    2.36.1
  85. Towards the Verification of Shell Scripts
    Mihaela Sighireanu and Ralf Treinen - IRIF, Université Paris-Diderot
    2.36.1
  86. Classification des 2-complexes
    Francis Lazarus et Arnaud de Mesmay - Gipsa-Lab, Grenoble
    2.38.1
  87. Call-by-value and call-by-name calculi: syntax, semantics, and logics
    Stefano Guerrini, Giulio Manzonetto - LIPN Paris 13
    2.1, 2.2
  88. Strong normalisation for simply typed lamba-calculus: a quest for new combinatorial proofs
    Stefano Guerrini, Giulio Manzonetto - LIPN Paris 13
    2.1,2.2
  89. Implémentation instrumentable du protocole IKEv2
    Pierre Néron - ANSSI Paris
    2-30, 2-4
  90. Vérification structurelle d'applications JavaCard
    Pierre Néron - ANSSI Paris
    2-7-2, 2-36-1
  91. Synthesis of Concurrent Implementations from Sequential Ones
    Ahmed Bouajjani, IRIF (LIAFA), Univ Paris Diderot, Bat Sophie Germain, Paris 13eme.
  92. 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)
  93. Model Checking on the fly for ATL*
    Serenella Cerrito-Ibisc (Evry)
  94. Information per time unit in timed systems
    E. Asarin and A. Degorre - IRIF
    2-8-2
  95. Compression of mixed (discrete-continuous) signals
    E. Asarin and A. Degorre - IRIF
    2-8-2
  96. Trier sur un cycle
    Christoph Dürr - LIP6
    2-24-[12]
  97. Formalizing Abstract Machines
    Beniamino Accattoli - INRIA Saclay, Parsifal team
  98. Protection of private information
    Catuscia Palamidessi and Kostas Chatzikokolakis – INRIA and Ecole Polytechnique
    2.3.2: Foundations of privacy
  99. Nids de serpents et arrangements de tuyaux
    Vincent Pilaud et Thibault Manneville - École Polytechnique
    2-38-1, 2-10
  100. Influence vs Reaction Systems
    François Fages
    2-19, 2-6,
  101. Boucles de rétroaction positive et multistationarité dans des systèmes de réactions
    Sylvain Soliman
    2-19, 2-35-1, 2-29-1
  102. Boolean Semantics of Reaction Systems with Inhibitors
    François Fages
    2-29, 2-6, 2-9-2
  103. Biochemical Program Compiler
    François Fages
    2-19,
  104. Performance study of making IDSs self-adaptable in IaaS clouds
    Christine Morin, Louis Rilling - IRISA / Inria Rennes
  105. 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
  106. Abstraction of Relations between Memory States
    Xavier Rival
    2.6
  107. Modèles de calculs à temps continu. Caractérisation de classes de complexité par systèmes dynamiques à temps continu.
    Olivier BOURNEZ
    2.33.1
  108. Transducteurs bidirectionnels en entrée et en sortie
    Olivier Carton & Olivier Serre (LIAFA)
  109. Games with Hierarchical Objectives
    Ocan Sankur - Irisa, Rennes
    1.22, 2.8, 2.9
  110. Lagrangian Duality in Online Algorithms
    Christoph Dürr and Nguyen Kim Thang, University Paris 6 and University Evry
  111. New Quantum Algorithms for k-Clique
    Frederic Magniez - IRIF (ex PPS-LIAFA), U. Paris Diderot
    2.34.1
  112. Composantes connexes d'un nœud dans un flot de liens
    Binh-Minh Bui-Xuan et Clémence Magnien, LIP6, UPMC, Paris.
  113. 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
  114. Intégration de la bibliothèque VTK dans l'environnement de développement de l'unité
    Grégory BAERT - Lille
  115. Vérification d'ordre supérieur et modèle stable
    Sylvain Salvati
    1-18; 1-20
  116. Caract ́erisation de formes : Invariants par rotation des formes quartiques
    Evelyne Hubert & Théo Papadopoulo, Inria Sophia Antipolis
    2.13.1; 2.22
  117. 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
  118. Generalizations of Binary Search: Finding a Target in Partially Ordered Sets
    Adrian Kosowski
  119. Algorithms for Global Illumination
    Venceslas Biri (UPEM, Universite Paris-Est) and Nabil Mustafa (ESIEE, Universite Paris-Est)
  120. Attack-defense trees for computer security: formal modeling of preventive and reactive countermeasures
    Barbara Kordy and Gildas Avoine - IRISA, Rennes
  121. Une sémantique catégorique de la logique de séparation concurrente
    Paul-André Melliès - PPS
  122. Trier sur un cycle
    Christophe Durr - P6
    2.24.2
  123. Root solver using subdivision and Fast Fourier Transform
    Guillaume Moroz, Marc Pouget, Rémi Imbach
    2.22 2.13.1
  124. Traitor tracing and trace-and-revoke systems based on the Learning-With-Errors problem
    Benoît Libert - ENS de Lyon
  125. Homomorphic encryption beyond semantic security
    Fabien Laguillaumie and Benoît Libert - ENS de Lyon