Internships 2022/2023

  1. Synthesis of reliable autonomous systems from unreliable components
    Danko Ilik - CNES Paris Daumesnil
  2. Datalog Reasoning and Explanation
    David Carral (david.carral@inria.fr) - Inria/LIRMM Montpellier
    1-39, 2.26.1
  3. Hybrid Reasoning Over Heterogenous Data
    federico ulliana (federico.ulliana@inria.fr)
    1-39, 2.26.1
  4. Fast algorithms for combinatorial optimization and machine learning
    Adrian Vladu, IRIF, Paris
  5. Improved Sparse Optimization for Machine Learning
    Adrian Vladu, IRIF, Paris
  6. Signatures post-quantiques fond´ees sur le MPC-in-the-Head
    Zoé Amblard, Aurélien Dupin, Thomas Ricosset
  7. Algorithme d'Euclide en temps constant pour la cryptographie
    Simon Abelard, Valentin Vasseur - Gennevilliers (92)
  8. Flux d'information et analyse de pureté: application à l'initialisation non-ambiguë de modules OCaml
    Benoît Montagu, Thomas Jensen, Épicure team, Inria Rennes
    2.4, 2.6
  9. Improving Diagnosis Quality and Performances of a Formal Verification Tool for Electric Circuits
    Matthieu Moy, LIP/Lyon or Verimag/Grenoble
  10. Dedicated Solver for Formal Verification of Electric Circuits with Multiple Power Supplies
    Matthieu Moy, LIP/Lyon or Verimag/Grenoble
    http://www.ens-lyon.fr/LIP/CASH/wp-content/uploads/2022/10/M2-SMT-avec-T-minimaliste.pdf
  11. Schnyder woods for higher genus surfaces, with application to graph drawing
    Luca Castelli Aleardi, Ecole Polytechnique (LIX)
    2.38.1, 2.10
  12. A COMMON FUTURE FOR TOURISM AND WATER RESOURCE: THE CASE OF CAT BA ISLAND
    Paul Bois / Cédric Gaucherel - Internship in Strasbourg
  13. Semantics and Implementation of Actors in Multicore OCaml
    Gabriel R ADANNE, Ludovic Henrio, Inria CASH/LIP
  14. Graphical Reasoning, in Coq
    Gabriel RADANNE, Yannick ZAKOWSKI – Inria CASH/LIP
  15. Compiler Intermediate Representation for Algebraic Data Types
    Gabriel RADANNE, Laure Gonnord – Inria CASH/LIP
  16. CFG Patterns: A new tool to formally verify optimisations in Vellvm
    Gabriel RADANNE, Yannick ZAKOWSKI – Inria CASH/LIP
  17. Cooperative task scheduling and synchronization
    Jean-Pierre Lozi - Inria Paris
  18. Graphical Language for Clifford Hermiticians in Quantum Computing
    Renaud Vilmart - LMF, Saclay
    Quantum information
  19. Optimisation automatique de l’implémentation de boîtes-S pour la cryptographie symétrique
    Sébastien DUVAL - Université de Lorraine, Nancy, France
  20. Types for complexity analysis in a process calculus
    Patrick Baillot - CRIStAL (Villeneuved'Ascq / Lille)
    2.3.1, 2.4
  21. Implicit computational complexity in Pi-calculus
    Patrick Baillot - CRIStAL (Villeneuved'Ascq / Lille)
    2.3.1, 2.4
  22. Research Internships @ Max Planck Institutes in Computer Science
    MPI-SP (Bochum), MPI-SWS (Saarbrucken and Kaiserslautern), MPI-INF (Saarbrucken)
  23. Symétries et extensions des intervalles de Tamari à travers des bijections
    Wenjie Fang et Éric Fusy - LIGM, Univ. Gustave Eiffel (Marne-la-Vallée)
    2.10, 2.15
  24. Internships in the Theory of Distributed Algorithms group, Algorithms & Theory branch at CISPA Helmholtz Center for Information Security, Saarbruecken
    Sebastian Brandt
  25. Usuba: high-speed, purely functional symmetric cryptography
    Pierre-Evariste Dagand, IRIF
    2.4
  26. Bayesian Inference and Let-Term Transformations
    Michele Pagani - IRIF Paris
  27. Catalan number and cylindric paritions
    Sylvie Corteel, Universite Paris Cite, corteel@irif.fr
    C2-10, C2-15
  28. Polymorphic records with union and intersection types and their application to the Elixir language
    Giuseppe Castagna - IRIF
    2.4
  29. Semantics and types for synchronous programming with state machines in a multi-periodic setting
    Patrick Baillot, Julien Forget, Sylvain Salvati - CRIStAL (Villeneuve d'Ascq / Lille)
    2.23.1, 2.4.2
  30. Algorithmique des isogénies de variétés abéliennes et cryptographie post-quantique
    Pierre-Jean Spaenlehauer (pierre-jean.spaenlehauer@inria.fr) - Inria Nancy, équipe CARAMBA
    Cryptologie, calcul formel.
  31. Interopérabilité vérifiée entre OCaml et C
    Armaël Guéneau - LMF, Saclay
    2.36.1
  32. The compositional structure of indefinite causal order
    Augustin Vanrietvelde - Inria Saclay
  33. Cybersecurity and Safety analysis by Abstract Interpretation with Frama-C / Eva
    Valentin Perrelle, CEA LIST, Palaiseau
    2.6 Abstract interpretation
  34. Types for sensitivity analysis and differential privacy in functional programming
    Patrick Baillot - CRIStAL (Villeneuved'Ascq / Lille)
    2.1, 2.3.2, 2.4
  35. Type invariants and ghost code for deductive verification of Rust code
    Jacques-Henri Jourdan - LMF Université Paris-Saclay
    2.4, 2.7.2, 2.36.1
  36. Synthesizing coalition strategies in parameterized concurrent games
    Patricia Bouyer, LMF, Saclay
    2.20.1 - 2.8.1
  37. Efficient Zero-Knowledge Proofs for all Programs
    Matthieu Rivain
    Cryptography
  38. Verification of security protocols - application to e-voting
    Stéphanie Delaune & Joseph Lallemand, IRISA (Rennes)
    2.30
  39. Implementation of hierarchies of algebraic structures in type theory
    Assia Mahboub, Cyril Cohen – Inria/LS2N, Nantes
    2.7.1, 2.7.2,2.4
  40. Vérification formelle de primitives cryptographiques post-quantiques
    Tristan Ninet, Thomas Ricosset, Eric Sageloli, Aymeric Fromherz - Gennevilliers (92)
  41. Reinforcement learning techniques for Multi-agent path finding with imperfect information
    Jilles Dibangoye, Ocan Sankur, François Schwarzentruber - Univ. Rennes, Irisa, Rennes
  42. Treillis de Tamari et arbres de parking
    Bérénice Delcroix-Oger - Matthieu Josuat-Vergès
  43. Deep Learning for improving formal verification with Frama-C / Eva
    Michele Alberti, CEA LIST, Palaiseau
  44. Faithful Nash equilibria in games over graphs
    Dietmar Berwanger, Patricia Bouyer
    2.20.1
  45. Computability and Complexity Theory for Models of Very Deep Learning.
    Olivier Bournez
  46. Programming with Ordinary Differential Equations and Continuous Time: Towards a programming language or pseudo-programming language.
    Olivier Bournez
  47. Optimisation de protocoles pour la verification de calculs quantiques delegues
    H. Ollivier / E. Kashefi
  48. Formally verified optimizations for safety-critical embedded code
    David Monniaux & Sylvain Boulmé, VERIMAG
  49. Measures against speculative attacks in a certified optimizing compiler
    David Monniaux & Sylvain Boulmé, VERIMAG
  50. Model Checking for Malware (Virus) Detection
    Tayssir Touili - Le Laboratoire d'Informatique de Paris-Nord (LIPN)
  51. Security counter-measures in a certified optimizing compiler
    David Monniaux & Sylvain Boulmé, VERIMAG
  52. Verified hash tables and hash-consing
    David Monniaux & Sylvain Boulmé, VERIMAG
  53. Static analysis of “pseudo-LRU” caches
    David Monniaux & Claire Maïza, VERIMAG
  54. Proof system interoperability
    Frédéric Blanqui - LMF
  55. Developing an Iris-Based Program Verification Framework for OCaml
    François Pottier, Inria Paris et Armaël Guéneau, Inria Saclay
    2.36.1, 2.7.1, 2.7.2
  56. Open Automata meet Session Types
    Ludovic Henrio, Inria CASH/LIP, Rabea Ameur-Boulifa, LTCI/Telecom Paris
  57. A type safe quantum programming language for quantum control and indefinite causal orders
    Romain Péchoux & Simon Perdrix
    2.34.1 2.1 2.4
  58. TAL et psychologie des émotions
    Alain Finkel
    1-31
  59. Reasoning with hard and soft constraints to repair and query inconsistent data
    Meghyn Bienvenu + Camille Bourgaux - LaBRI, Bordeaux
    Web data management
  60. Programmation par contraintes pour la résolution de problèmes de cryptographie symétrique
    Marine Minier
    Cryptography
  61. Implémentation d'attaques cryptographiques
    ANSSI Crypto Lab, Paris 15
  62. Introduction of timing aspects into Event-B
    Amel Mammar, Idir Ait-Sadoune, Télécom SudParis, SAMOVAR/METHODES, Paris-Saclay University, LMF
  63. Introduction of timing aspects into Event-B
    Amel Mammar, Idir Ait-Sadoune - Télécom Sud-Paris & Centrale-Supélec
  64. Vérification automatique pour la sûreté des systèmes
    David CHEMOUIL (ONERA DTIS, Université de Toulouse)
  65. Extensions de la méthode formelle Alloy d’analyse de systèmes
    David CHEMOUIL (ONERA DTIS, Université de Toulouse)
  66. Towards Law versioning: a double category of XML files
    Luc Pellissier — LACL, Université Paris Est Créteil
    2.2 2.4
  67. Multi-objective optimization for the vehicule rescheduling problem
    François Schwarzentruber, Ocan Sankur
    2.24.1, 2.24.2
  68. Static Analysis under a Given Time Budget
    Raphaël Monat – Inria @ University of Lille
    2.6
  69. Incremental Static Analysis
    Raphaël Monat – Inria @ University of Lille
    2.6
  70. Distilling Bell-nonlocality for quantum cryptography
    Jean-Daniel Bancal, Peter Brown and Mirjam Weilenmann – IPhT CEA Saclay and LTCI Télécom-Paris
    2.34.1, 2.34.2 (and tangentially 1-37 convex optimization)
  71. Network-based biomarker discovery of Parkinson’s disease at various stages
    Julie Coloigner, IRISA, Rennes
  72. Feerated learning with untrusted server
    Jan Ramon - INRIA-Lille
    cryptography
  73. Stage - BAC+5 - Ingénieur.e simulation quantique de la chimie des batteries (H/F)
    Nassima Benammar, Thomas Chapuis- Guyancourt
  74. Parameterized complexity : A tool to handle multiobjective problems
    Julien Baste; Laetitia Jourdan; Université de Lille
    2.11.1 Parameterized Complexity
  75. Safety Analysis of Real-Time Discrete-Event and Hybrid Systems
    Philippe Dague et Lina Ye - LMF, Université Paris-Saclay
    2.8.2
  76. Centres and Commutants of Strong Monads
    Vladimir Zamdzhiev, Louis Lemonnier - LMF, Université Paris-Saclay
    2.2
  77. Cybersecurity high assurance Software
    Yacine Bouguechal - Thales Gennevilliers
  78. Query-Directed Width Measures for Probabilistic Graph Homomorphisms
    Antoine Amarilli and Mikaël Monet - Télécom Paris or Inria Lille
  79. Design and Implementation of User-Friendly Concurrent Processes Description Language, and CTL* Model-Checker
    Vincent Hugot & Pascal Berthomé – INSA CVL, campus de Bourges
    Automata and Formal Languages, System Programming, Analysis, and Verification
  80. Infinite Structures for Program Verification
    Aymeric Fromherz and Théo Laurent, INRIA Paris
  81. Semantics of Boolean Networks
    Philippe Dague et Thomas Chatain - LMF, Université Paris-Saclay, CNRS, ENS Paris-Saclay
  82. Categorical semantics of ordered linear logic, for a reconstruction of ownership in programming languages
    Guillaume Munch-Maccagnoni, Inria, Nantes
    2.2, 2.1, (2.4)
  83. Ordered algebraic data types in systems programming languages
    Guillaume Munch-Maccagnoni, Inria, Nantes
    2.4, (2.2, 2.1)
  84. Real-time analysis and verification of ROS2 robotic applications
    M. Foughali; P-E Hladik. LS2N (Nantes) & IRIF (Paris)
  85. Extending Artificial Intelligence Verification and Validation to Coverage Properties
    Zakaria Chihani
  86. Sparse and robust training for neural network verification
    Augustin Lemesle
  87. Specification from Generative Models for Machine Learning Verification
    Julien Girard-Satabin
  88. History-Deterministic Timed Automata
    Uli Fahrenberg, Nicolas Markey – IRISA, Univ. Rennes
    2.8.2, 2.20.1
  89. Security ceremonies
    Barbara FILA, IRISA, France
    formal modeling, security protocols, formal methods, security, verification
  90. Vérification formelle de logiciels critiques en instrumentation spatiale
    Hai Nguyen Van, Xavier Thirioux, ISAE-SUPAERO, Toulouse
    2.5.1., 2.6, 2.7.2, 2.23.1
  91. Conjecture sur la relation entre les interprétations stochastiques et continus des processus de réactions en présence de règles de synthèse.
    François Fages Inria Saclay - Ecole Polytechnique
    2.19, 2.6, 2.3.1
  92. Energy/performance tradeoff of ML-enhanced high-speed networks
    Leonardo LINGUAGLOSSA - Telecom Paris (Institut Polytechnique de Paris)
  93. Decentralized Clustered Federated Learning
    Giovanni Neglia - Sophia Antipolis
  94. Federated Learning for Heterogeneous Model Architectures
    Giovanni Neglia, Inria, Sophia Antipolis
  95. Question Answering With Open Knowledge Bases
    Julien Romero, Oana Balalau. Location: Télécom SudParis, Palaiseau
  96. Deep Graph Neural Networks (GNNs) and Applications
    Fragkiskos Malliaros (CentraleSupelec, Inria) and Jhony Giraldo (Telecom Paris, IP Paris)
  97. Descriptive complexity of topological invariants
    Mathieu Hoyrup, Loria, Nancy
  98. Reliable numerical integration
    Joris van der Hoeven, Grégoire Lecerf, LIX, Polytechnique
    Advanced complexity, Software engineering, Polynomial systems, computer algebra and applications, Efficient algorithms in computer algebra,
  99. On the convergence of iterative sampling methods and the detection of meta-stable states in dynamical systems
    Frederic Cazals; Inria Sophia Antipolis
    2.11 2.14.1 2.15
  100. Formal Methods for the Verification of Self-Adapting Distributed Systems
    Radu Iosif, Arnaud Sangnier
  101. Formal Methods for the Verification of Self-Adapting Distributed Systems
    Radu Iosif, Arnaud Sangnier - Verimag, Grenoble
  102. Compilation of a DSL based on transducers to SIMD optimized programs
    Charles Paperman and Gabriel Radanne