Internships 2020/2021

  1. State-based attack-defense trees
    Sophie Pinchinat and Barbara Fila (IRISA, Rennes, France)
  2. IRM de diffusion et relaxométrie : vers une utilisation combinée
    Olivier Commowick
  3. Probabilistic Functional Programs: Termination and Verification
    Charles Grellois - Aix-Marseille Université
    mainly 2.4, and also 2.2, 2.1
  4. Catala: Moving Towards the Future of Legal Expert Systems
    Denis Merigoux – Karthikeyan Barghavan – Paris
  5. Quantum controlofsuperconducting circuits using neural networks
    Benjamin Huard & Audrey Bienfait - Laboratoire de Physique, ENS de Lyon
    Quantum Information
  6. Fair Online Classification with Partial Feedback
    Nicolas Gast and Patrick Loiseau - Inria/LIG (Grenoble)
  7. Online Algorithms for Fair Ad Auctions
    Nicolas Gast and Patrick Loiseau - Inria/LIG (Grenoble)
  8. A mathematical analysis of positive discrimination mechanisms in multi-dimensions
    Patrick Loiseau and Bary Pradelski, Inria/LIG (Grenoble)
  9. Fair transactions ordering in a blockchain
    Krishna Gummadi and Patrick Loiseau - MPI-SWS (Saarbruecken, Germany)
  10. Théorie des algorithmes : étude comparée
    Julien Cervelle - LACL - Université Paris-Est Créteil
  11. Analyse physique d’une signature post-quantique fondée sur les réseaux euclidiens
    Thomas Ricosset, Ange Martinelli et Mélissa Rossi (Thales Gennevilliers et ANSSII)
    2.12.1
  12. Implementing a differentiable programming framework based on linear logic and functional programming
    Michele Pagani
    2.1 or 2.2 or 2.4
  13. Specification and Verification of a Transient Data Structure
    Arthur Charguéraud et François Pottier - Paris ou Strasbourg
    2.4, 2.7.1, 2.7.2, 2.36.1
  14. Hint Typing, Optimistic Compilation of Dynamic Languages
    Manuel Serrano, Inria Sophia Antipolis
  15. Profile-Guided optimization for Dynamic Languages
    Manuel Serrano, Inria Sophia Antipolis
  16. Secure wallet application for cryptocurrency and blockchain transactions
    Matthieu Rivain, Aleksei Udovenko and Junwei Wang
  17. Leakage-Resilient Modes of Operation for Authenticated Encryption
    Sonia Belaïd and Matthieu Rivain
  18. FPGA Prototype of a Custom Variable Precision Processor
    mailto:Cesar.FUGUETTORTOLERO@cea.fr
  19. Behavioural Model of a Variable Precision Arithmetic Accelerator
    Cesar.FUGUETTORTOLERO@cea.fr
  20. FPGA Prototype of a Custom Variable Precision Processor
    mailto:Cesar.FUGUETTORTOLERO@cea.fr
  21. Enhance the security of networking libraries with formally proven message handling in SPARK
    The internship will take place in the offices of AdaCore in Paris and will be supervised by Yannick Moy. Application at: internships@adacore.com
  22. Prove the robustness and functionality of critical units of the SPARK standard library
    Mailto: internships@adacore.com. Location: Paris or Toulouse
  23. Compiling by interpreting: case of buffer allocation functions
    Christophe Alias
  24. Analyse de déformations et recherche de correspondance pour les protéines HLA
    Etienne Corman
  25. Combining implicit and explicit surface representations for 3D human reconstruction from a single image
    Dr. Adnane Boukhayma - INRIA Rennes
  26. Toward a scalable and accurate network calculus
    Anne Bouillard (Huawei Technologies, France, Boulogne-Billancourt)
    2.17.1
  27. Toward an accurate stochastic network calculus
    Anne Bouillard (Huawei Technologies, France, Boulogne-Billancourt)
    2.17.1
  28. Complexity theory with Discrete Differential Equations/Finite differences.
    Olivier Bournez
  29. Characterization of NP or PSPACE with polynomial Ordinary Differential Equations Continuous time Analog machines and models of computation.
    Olivier Bournez
  30. Graph summarizing using quasi-cliques
    Baste/Haddad/Seba-Lyon/Lille
  31. Graph Sparsification
    Habib/Haddad/Seba-Lyon
  32. Génération réaliste de paquets réseau pour l’évaluation de détecteurs d’intrusion
    G. Blanc (IMT, IP Paris), Ludovic Mé (Inria), PF Gimenez (CentraleSupélec), F. Majorczyk (DGA-MI) - Rennes
  33. Automated binary-level program analysis for software security
    Sébastien Bardin
  34. A Semantical Study of the Least-Level Strategy in the Bang Calculus
    Delia Kesner (IRIF, Univ. de Paris) - Giulio Guerrieri (Univ of Bath)
  35. Verification of security protocols: application to e-voting
    Stéphanie Delaune and Joseph Lallemand - IRISA/Rennes
    2.30
  36. Verification of security protocols: Squirrel prover
    David Baelde (LSV/Université Paris Saclay) et Stéphanie Delaune (IRISA/Rennes)
    2.30
  37. A stream language for polynomial time over the reals
    Emmanuel Hainry and Romain Péchoux
    2.1, 2.4, and 1.17 (english upon request)
  38. Automatic complexity analysis of probabilistic programs
    Emmanuel Hainry and Romain Péchoux (LORIA, Nancy)
    1.17, 2.11.2, and 2.4 (english upon request)
  39. Characterizing Quantum complexity classes
    Emmanuel Hainry and Romain Péchoux (LORIA, Nancy)
    1.17, 2.34
  40. Operational Game Semantics for OCaml Type System
    Guilhem Jaber - Université de Nantes
    1-20, 2-2, 2-4
  41. Specifying and reasoning about preferences over inconsistent knowledge bases
    Meghyn Bienvenu (LaBRI, Bordeaux) & Camille Bourgaux (DI ENS, Paris)
    Logical aspects of artificial intelligence, Web data management
  42. Stratégies de compilation pour la synthèse de circuits
    Christophe Alias - LIP/ENS de Lyon
    Compilers, computer architecture
  43. High-performance compilation schemes using dynamic analysis
    Christophe Alias - LIP/ENS de Lyon
    Compilers, computer architecture
  44. Types for combining polynomial time programs
    Patrick Baillot, LIP, ENS de Lyon
    2.1, 2.2, 2.4
  45. Axiomatic in phylogeny-reconstruction distance-based methods and flat clustering with overlap
    Celine Scornavacca, Christophe Paul, Dimitrios Thilikos -Montpellier
  46. Atlas de texture à coutures invisibles
    Dmitry Sokolov - Nancy
  47. Elliptic mesh smoothing
    Dmitry Sokolov - Nancy
  48. Génération de maillage hexahédral structuré par blocks
    Dmitry Sokolov - Nancy!
  49. Information per time unit in timed systems
    Eugene Asarin - IRIF (Paris)
    2.8.2, 2.20.2
  50. Learning hybrid automata
    E. Asarin, P. Habermehl - IRIF (Paris)
    2.8.2
  51. Timed distances
    E. Asarin, A.Degorre - IRIF (Paris)
    2.8.2, 1.22
  52. Meta reinforcement learning
    Nathanaël Fijalkow et Charles Grellois ; stage à Aix-Marseille
  53. Fast Secure Computation Meets Linear-Time Encodable Codes
    Geoffroy Couteau - IRIF, Université de Paris
    2.13.2, 2.12.1
  54. Non-commutative logic and categorical semantics for systems programming languages
    Guillaume Munch-Maccagnoni, Inria, Nantes
    2.1, 2.2, 2.27.1, (2.4, 2.36.1)
  55. Modélisation et vérification en logique temporelle du premier ordre
    Julien Brunel, David Chemouil
  56. Alt-Ergo on the bench
    L'équipe de développement d'Alt-Ergo - Paris 14
  57. Alt-Ergo Fuzz
    L'équipe de développement d'Alt-Ergo, OCamlPro, Paris 14
  58. Alt-Ergo for the Win(dows)
    L'équipe de développement d'Alt-Ergo, OCamlPro, Paris 14
  59. Détection de fonction identité à la compilation
    Vincent Laviron ou Pierre Chambart, OCamlPro, Paris 14
  60. Généralisation de la Récursion terminale modulo constructeur
    Vincent Laviron ou Pierre Chambart, OCamlPro, Paris 14
  61. Améliorations pour l’application web Try OCaml
    Louis Gesbert et Raja Boujbel, OCamlPro, Paris 14
  62. Interface Graphique pour la Gestion de Paquets d’OCaml
    Louis Gesbert et Raja Boujbel, OCamlPro, Paris 14
  63. A Principled Investigation of the Lottery Ticket Hypothesis for Deep Neural Networks
    Adrian Vladu, IRIF, Paris
  64. AI Safety internship at CEA Saclay
    Zakaria Chihani
    2.36.1 Proofs of programs ; 2.35.1 Constraint programming ; 2.9.2 Algorithmic verification of programs 2.7.2 Proof assistants ; 2.7.1 Foundations of proof systems ; 2.5.1 Automated deduction ; 2.6 Abstract interpretation: application to verification and static analysis ;2-4 Functional programming and type systems ; 1-36 Initiation to research ; 1-39 Logical aspects of artificial intelligence ;1-22 Basics of verification ; 1-35 Introduction to Computer Vision ;
  65. Improved Algorithms for Combinatorial Discrepancy
    Adrian Vladu, IRIF, Paris
  66. Solvability in Call-by-Push-Value
    Delia Kesner (IRIF, Univ. de Paris) - Giulio Guerrieri (Univ of Bath)
  67. Automated reasoning in a meta-logic for cryptographic protocols
    David Baelde and Adrien Koutsos
  68. Searching with predictions
    Spyros Angelopoulos- LIP6, Sorbonne University
  69. Vision-based robot localisation with a quantum algorithm
    Ezio MALIS - Inria Sophia Antipolis
  70. FORMAL MECHANICAL MODELS FOR DISTRIBUTED COMPUTING – LUMINOUS ROBOTS
    P. Courtieu/X. Urbain/X. Défago – Lyon
  71. MODÈLES MÉCANIQUES FORMELS POUR L’ALGORITHMIQUE DISTRIBUÉE - COMPORTEMENTS PROBABILISTES
    P. Courtieu/X. Urbain/S. Tixeuil - Lyon/Paris
  72. MODÈLES MÉCANIQUES FORMELS POUR L’ALGORITHMIQUE DISTRIBUÉE - PROCÉDURES DE DÉCISION ET SEMI-DÉCISION
    P. Courtieu/X. Urbain/E. Coquery - Lyon/Paris
  73. MODÈLES MÉCANIQUES FORMELS POUR L’ALGORITHMIQUE DISTRIBUÉE - GÉOMÉTRIE NON EUCLIDIENNE / APPROCHÉE / INCERTAINE
    S. Brandel/X. Urbain/L. Rieg - Lyon/Grenoble
  74. UN DEMONSTRATEUR POUR LA LOGIQUE DE LA CAPABILITE (ABILITY LOGIC)
    Nicola Olivetti et Charles Grellois, Aix-Marseille Université
  75. Compiler support for data-driven parallelism
    Christophe ALIAS, Jean Baptiste BESNARD, Patrick CARRIBAULT et Julien JAEGER
    compilation, code optimisation
  76. Analyse automatisée de binaires appliquée à la recherche de vulnérabilités matérielles
    Antoine Rollet - Bordeaux
  77. De la synthèse de programmes aux tests, et vice-versa!
    Nathanaël Fijalkow et Antoine Rollet - LaBRI Bordeaux
  78. Testing Deep Neural Networks
    Antoine Rollet - LaBRI Bordeaux
  79. Analyse automatisée de binaires appliquée à la recherche de vulnérabilités matérielles
    SERMA:Julien BERNET et Michael GRAND, LaBRI: Antoine ROLLET et Grégoire SUTRE - Bordeaux
  80. Synthèse et apprentissage de réseaux booléens prédictifs pour la différenciation cellulaire
    Loïc Paulevé - LaBRI (Bordeaux)
  81. From Law To Code: Trust and Proof
    Hugo Gimbert and Sonia Desmoulins-Canselier
    Verification
  82. Robotics-inspired methods to model RNA molecules
    Juan Cortes LAAS Toulouse, Loic Salmon CRMN Lyon
  83. Energy-aware scheduling under topological constraints
    E. Bampis, F. Pascual, G. Lucarelli - LIP6 Sorbonne Université
    2.24.1
  84. Enumerating Query Results on Multitrees
    Antoine Amarilli, Louis Jachiet, Luc Segoufin, École normale supérieure
    2.26.1 Logique, complexité descriptive, théorie des bases de données ; 2.26.2 Gestion de données du Web
  85. Internships at Several Max Planck Institutes
    Saarbrücken, Kaiserslautern, Bochum, Remote
  86. Homomorphic Compiler
    Pascal Paillier and Benoit Chevallier-Mames
    Crypto, FHE
  87. Uncovering the sources of French classical theater through automatic text alignment and comparison
    Philippe Gambette - LIGM
    1.32, 2-24-2, 2-29-1, 2-29-2
  88. Deep learning for online speaker diarization
    Hervé Bredin / CNRS/IRIT (Toulouse)
  89. Deep audio representation learning
    Hervé Bredin / CNRS/IRIT (Toulouse)
  90. Robust and adaptive data-driven anomaly detection in IoT
    Sébastien Tixeuil (LIP6), Gregory Blanc (Télécom SudParis) - LIP6, Paris
  91. Data-driven assessment of intrusion detection
    Sébastien Tixeuil (LIP6), Gregory Blanc (Télécom SudParis) - LIP6, Paris
  92. Programmation Linéaire pour la reconstruction de génomes à partir demétagénomes: modélisation, tests, passage à l’échelle
    S. Chaffron, G. Fertin, G.Jean
  93. Aspects Algorithmiques de l’Inférence de Protéines
    G. Fertn, G. Jean
  94. Quantum Annealing pour le deep hedging
    Joseph MIKAEL (EDF Lab)
  95. Classification sur TensorFlow Quantum
    joseph.mikael@edf.fr
  96. Combinatorial Structures for Bounded-Memory Computing
    Petr Kuznetsov (Telecom Paris)
    2.18.2, 2.18.1
  97. Blockchain or not Blockchain? Costs and benefits of large-scale synchronization
    Petr Kuznetsov (Telecom Paris), Luis Belmar Letelier (Mazars)
    2.18.2, 2.18.1
  98. Hybrid Relaxed Concurrent Data Structures
    Petr Kuznetsov (Telecom Paris), Armando Castaneda (UNAM)
    2.18.2
  99. Agreement and Clustering in Spiking Neural Networks
    Petr Kuznetsov (Telecom Paris), Denis Sheynikhovich (UPMC)
  100. Verifiable Delay Functions for Permissionless Replication
    Duong Hieu Phan (Telecom Paris), Petr Kuznetsov (Telecom Paris)
  101. Research on FHE and Concrete lib
    Ilaria Chillotti and Damien Ligier - Paris
  102. Compression de graphes par parcours avec Webgraph
    Fabien de Montgolfier - IRIF, Paris
    Graph algorithms
  103. Compression de graphes bipartis par décomposition bimodulaire
    Fabien de Montgolfier - IRIF, Paris
    Graph algorithms
  104. Hierarchical Query-Aware Graph Summarization
    Angela Bonifati & Stefania Dumbrava - Lyon/Paris and/or online
    2.29.1 Algorithmique des graphes; 2.26.2 Gestion de données du web
  105. Incremental Schema Inference for the Covid-19 Dataset
    Angela Bonifati (Univ Lyon 1, LIRIS - Lyon) & Stefania Dumbrava (ENSIIE, Samovar - TelecomSud Paris - Paris)
    2.29.1 Algorithmique des graphes; 2.26.2 Gestion de données du web
  106. Compilateur dédié à l’évaluation de requêtes SQL
    Jean-Marie Lagniez, Pierre Senellart (ENS, Paris ou CRIL, Lens)
    2-26-2
  107. State-of-art type checking for the Elixir programming language
    Giuseppe Castagna and José Valim, Institut de Recherche en Informatique Fondamentale and Dashbit
    2.4
  108. Tropical geometry applied to the analysis of interior point methods
    Xavier Allamigeon and Stéphane Gaubert
    2.20.1; 2.24.1
  109. Etude des approches pour le contrôle des fermes éoliennes par l'apprentissage par renforcement
    Ana Busic (Inria Paris et DIENS, PSL); Jiamin Zhu et Domenico Di Domenico (IFP Energie nouvelles)
    2.17.1
  110. \Performance Evaluation and Optimization of Energy Packets Networks
    Location: Inria Paris; Supervisors: Ana Busic (Inria Paris et DIENS, PSL); Jean-Michel Fourneau (DAVID - UVSQ, Paris Saclay); Josu Doncel (University of the Basque Country)
    2.17.1
  111. Dynamic matching and reinforcement learning
    Ana Busic (Inria Paris et DIENS, PSL)
    2.17.1; 2.24.1
  112. Semantics of a low-level language for verified computer algebra
    Guillaume Melquiond, Inria, Université Paris Saclay
    2.7.2, 2.36.1
  113. Estimation analytique des probabilités de phénotypes alternatifs en biologie
    Aurélien Naldi, François Fages - Inria Saclay
  114. Conditions de stabilité qualitative des acteurs clés de processus biologiques
    Aurélien Naldi, François Fages - Inria Saclay
  115. Interval Arithmetic for Ordinary Differential Equation Systems
    F. Fages, M. Hemery Inria Saclay
    C2-19 C2-6 C2-33-3 2-13-1
  116. A formal proof of correctness of Tail-Recursion Modulo Constructor in the Iris logic
    Léo Stefanesco, François Pottier, Gabriel Scherer, Frédéric Bour - INRIA Paris
    2.4, 2.7.2 2.36.1
  117. Introducing compound components in JavaBIP
    Simon Bliudze, Inria Lille - Nord Europe
  118. Composability & verification of BIP design patterns
    Simon Bliudze, Inria Lille - Nord Europe
  119. Verification of hybrid synchronous/asynchronous systems
    Simon Bliudze, Inria Lille - Nord Europe
  120. Bacterial Consensus
    Matthias Függer (LMF), Thomas Nowak (LISN)
  121. Time-Accurate Network Simulation Interconnecting VMs with Hardware Virtualization towards stealth analysis
    Martin Quinson (ENS Rennes), Louis Rilling (DGA-MI), Matthieu Simonin (Inria) – Rennes
  122. Decision Procedures for Inductive Separation Logic Modulo Data Theories
    Nicolas Peltier, Radu Iosif - Grenoble
  123. Proving Correctness of Reconfigurable Systems
    Radu Iosif - Grenoble
  124. Étude d’une méthode probabiliste d’estimation de paramètres pour un modèle continu de dynamique de population océanique
    Benoit Delahaye et Guillaume Cantin - Laboratoire des Sciences du Numérique de Nantes (LS2N)
  125. Semantics of Cryptographic Proofs.
    David Baelde, Adrien Koutsos, Guillaume Scerri - Inria Paris
    2.30
  126. Predictive optimization of data transfers for Cloud File Providers on macOS/iOS
    Jean-Gabriel Morard, Apple, Paris
    Concurrency, Probabilistic aspects of computer science
  127. Unsupervised Domain Adaptation in Neuroimaging - The case of White Matter Lesions Segmentation
    Francesca Galassi, Nicolas Courty (Inria Rennes)
  128. Listing Graphlets in Real-World Graphs
    Mauro Sozio, Telecom Paris (Palaiseau), LINCS (Paris)
    Graph Mining
  129. Graph Clustering: Theory and Practice
    Mauro Sozio, Telecom Paris (Palaiseau), LINCS (Paris)
    Graph Mining
  130. Correlations in Networks: Beyond Quantum Theory
    Marc-Olivier Renou - Antonio Acin - Barcelona
  131. Un analyseur flots de données paramétré par un ordre d'itération pour le compilateur formellement vérifié CompCert
    Sandrine Blazy - Rennes
    2-04, 2-06, 2-07-1, 2-07-2, 2-36-1