Submit an internship offer

1. Reconnaissance de programmes par réseaux de neurones de graphes
   Sid Touati et Christophe Alias (INRIA Sophia Antipolis ou INRIA Lyon)
   
2. Formal Verification of Security Protocol
   Charlie Jacomme, Inria Nancy
   2.30, 2.7.2, 2.12.1
3. Using Model Checking for verifying Nuclear Power Plant Operating Procedures
   Valentin RYCHKOV, Claudia PICOCO, 91120 EDF R&D, Palaiseau
   1.22 Basics of verification, 2.8.2 Cyber-physical systems and their verification
4. Counter example and adversarial attacks for neural network verification
   Augustin Lemesle - Saclay
   
5. Formal reasoning training example generation for large language models
   Damien Sileo - Lille
   Logic, Planning, Learning
6. Pairs of square-free arithmetic progressions in infinite words
   Pascal Ochem and Matthieu Rosenfeld - at LIRMM, Montpellier
   
7. NP (non-deterministic polynomial time) & Analog computations.
   Olivier Bournez
   2.33.3
8. Complexity Theory for Models of Deep learning. Complexity Theory for Models of Very Deep learning.
   Olivier Bournez
   2.33.3
9. Numerical Analysis and Optimization of Functional Array Programs
   Thomas Koehler and Eva Darulova – ICube Laboratory, Strasbourg, France or Uppsala University, Sweden
   
10. Exploring Accuracy and Performance Trade-offs in Functional Array Programs
    Thomas Koehler and Eva Darulova – ICube Laboratory, Strasbourg, France or Uppsala University, Sweden
    
11. Algorithmes d'énumération dans les graphes
    Pierre Bergé and Vincent Limouzy - CLERMONT-FERRAND
    Parameterized algorithms and complexity (2.11.1), Advanced graph theory (2.29.1)
12. Optimizing Programs with Sketch-Guided Polyhedral Compilation
    Thomas Koehler and Christophe Alias – ICube Laboratory, Strasbourg or LIP Laboratory, Lyon
    
13. Génération automatique de clé de détermination pédagogiques
    Simon Castellan (Inria Rennes) ; Agnès Schermann (EcoBio, Univ Rennes 1)
    
14. Reproducing brain imaging pipelines to study analytical variability
    Boris Clénet, Camille Maumet, Unité Empenn U1228, INSERM, INRIA, Université Rennes, IRISA, UMR CNRS 6074
    
15. Formal modeling of security ceremonies
    FILA Barbara, IRISA, Rennes
    
16. Formal risk analysis of privacy-preserving data publishing algorithms
    ALLARD Tristan, IRISA, Rennes
    
17. Méthodes symboliques pour la bi-déduction dans le contexte de la vérification de protocoles de sécurité
    David Baelde (PR ENS Rennes) et Delaune Stéphanie (DR CNRS) - IRISA (Rennes)
    2.30; 1.33
18. Analyse formelle de sécurité des protocoles DRM
    Stéphanie Delaune & Joseph Lallemand, IRISA, Rennes
    2.30
19. Multi-Perspective Reasoning with Standpoint Logic
    Lucia Gomez Alvarez, Inria Centre at the University Grenoble Alpes
    
20. Optimization of minimizer-based k-mer partitioning for genomic sequences
    Camille Marchet (CNRS), Florian Ingels - CRIStAL, Lille
    
21. Vérification de propriétés sur les graphes temporels - vers un métathéorème
    Nathalie Sznajder, Binh-Minh Bui-Xuan – LIP6, SU UPMC.
    
22. Causality-aware temporal graphs with connectivity constraints
    Binh-Minh Bui-Xuan, Marcelo Dias de Amorim – LIP6, SU UPMC.
    
23. Reconstruction de mots par requêtes avec poids
    Gwenaël Richomme et Matthieu Rosenfeld
    
24. Verification of probabilistic properties for AI
    Eric Goubault and Sylvie Putot - LIX, Palaiseau
    
25. Quantified reachability properties for provably explainable AI
    Eric Goubault and Sylvie Putot - LIX, Palaiseau
    
26. Modélisation informatique des erreurs de décisions d’un opérateur humain en aviation ou en médecine
    Pr. Frédéric Boulanger (LMF, CentraleSupélec, Université Paris-Saclay) and Pr. Nicolas Sabouret (LISN, Université Paris-Saclay)
    Logical Aspects of Artificial Intelligence,
27. Evaluating the Experimental Complexity of Program Analysis
    Raphaël Monat (Inria Lille)
    2.6
28. Combining Query Languages and Semantic Analysis by Abstract Interpretation to Verify Program Correctness
    Antoine Miné - APR, LIP6, Sorbonne Université
    2.6
29. Verification of Unsafe Code in Rust Programs by Abstract Interpretation
    Antoine Miné - APR, LIP6, Sorbonne Université
    2.6
30. On Byzantine fault tolerance in dynamic networks
    Binh-Minh Bui-Xuan, Sébastien Tixeuil – LIP6, SU UPMC.
    
31. Algorithmic aspects of arithmetic theories with division
    Alessio Mansutti - IMDEA Software Institute
    
32. Analysing Petri Nets with Higher Dimensional Automata
    Hugo Bazille, Philippe Schlehuber-Caissier - Telecom SudParis (Courcourrones)
    
33. Static Analysis by Abstract Interpretation of Library Bindings in Multi-Language Applications
    Antoine Miné - APR, LIP6, Sorbonne Université
    2.6
34. Attaques par canaux auxilliaires en crypto fondée sur les réseaux
    Thomas Ricosset - Thales Gennevilliers
    2.12.1 2.12.2 2.13.1 2.13.2
35. Méthode d'extraction de clé à partir de distingueurs
    Nicolas DAVID
    2.12.1 2.12.2
36. Développement et intégration de primitives cryptographiques dans OpenSSL
    Sylvain Lacharte - Thales Cholet
    
37. Optimal stopping theory with predictions
    Spyros Angelopoulos- ILLS, Montreal, Canada
    2-24-1, 2-11
38. Energy Problems for ω-automata
    Philipp Schlehuber-Caissier, Sven Dziadek - Telecom SudParis
    
39. Online storage management with predictions
    Christoph Dürr - Sorbonne University
    2-24-1
40. Calculer avec les nombres à virgule flottante dans un contexte critique
    Danko Ilik - CNES - Paris
    
41. Quantum Distributed Algorithms
    Marc-Olivier Renou
    2.18.1, 2.34.1
42. Various topics in proof assistants, logic, and constructive mathematics
    Yannick Forster, Paris
    2-7-1, 2-7-2, 2-4
43. Local rewrite rules in type theory
    Théo Winterhalter — ENS Paris Saclay
    2.7.1, 2.7.2
44. Advanced Search Algorithms for Program Synthesis
    Nathanaël Fijalkow, Gabriel Bathie, Bordeaux
    
45. Dolev-Yao-Model-Guided Fuzzing of Cryptographic Protocols
    Lucca Hirschi
    2.30
46. https://members.loria.fr/LHirschi/pdfs/UKano_Lucca-Hirschi.pdf
    Lucca Hirschi, Inria Nancy
    2.30
47. Solving diversity problems
    Julien Baste - Université de Lille
    
48. Fixed-point implementation of Falcon and FN-DSA
    Thomas Prest - PQShield SAS (Paris, FR)
    2.12.2 - Arithmetic algorithms for cryptology
49. Implementation security of post-quantum digital signatures
    Antoon Purnal - PQShield (Remote, or Paris, France)
    2.12.2 - Arithmetic algorithms for cryptology
50. Cryptographic watermarking for preventing deepfakes in media data
    Thomas Prest, Thomas Espitau, Pierre-Yves Strub, Adrian Thillard - PQShield SAS (Paris, France)
    2.12.2 - Arithmetic algorithms for cryptology
51. Programme slicing pour Catala
    Vincent Botbol, Louis Gesbert, Romain Primet – Paris 1e=3e (INRIA)
    Abstract interpretation; Functional programming and type systems
52. Développement de protocoles cryptographiques pour un vote électronique (plus) sûrs dans la vraie vie
    Alexandre Debant
    Proofs of security protocols
53. Data selection and Shapley value in the linear case
    Patrick Loiseau (FairPlay team: Inria Saclay / ENSAE / Criteo)
    
54. Matching markets: the role of correlation on efficiency and equity
    Patrick Loiseau (FairPlay team: Inria Saclay / ENSAE / Criteo) and Bary Pradelski (Oxford / CNRS)
    
55. Safe Composition of Jasmin & Rust for High-Assurance Cryptography
    Vincent Laporte, Inria Nancy
    2.4, 2.6, 2.36.1
56. Exact Register Allocation in the Jasmin Certified Compiler
    Vincent Laporte, Inria Nancy
    
57. Formally Verifying Privacy in Cryptographic Protocols through Trace Properties
    Lucca Hirschi, Inria Nancy
    2.30
58. Reasoning over Bounded First-Order Logic Ontologies
    David Carral - Inria Montpellier
    
59. Étude et optimisation de la consommation énergétique des systèmes blockchain
    Rouwaida ABDALLAH - CEA-LIST
    
60. Embedded Machine Learning Programming (with potential PhD continuation)
    Inria Paris
    
61. Logic for differential privacy of functional programs
    Patrick Baillot - CRIStAL, Lille
    2.2, 2.7.1, 2.3.2
62. Exploring the functoriality of approximate posteriors for sheaf-structured models
    Grégoire Sergeant-Perthuis, LCQB Sorbonne Université
    
63. Kleene Algebra with Tests for probabilistic programs
    Patrick Baillot, Leandro Gomes - CRIStAL, Lille
    
64. Reasoning on the execution time of programs with Kleene Algebra with Tests
    Patrick Baillot, Leandro Gomes - CRIStAL, Lille
    
65. Identification versus anonymisation from an embedded client operating on a blockchain
    Christine Hennebert - GRENOBLE
    
66. Semantics and types for synchronous programming with state machines in a multi-periodic setting
    Patrick Baillot, Julien Forget, Sylvain Salvati - CRIStAL, Lille
    2.23.1, 2.4
67. Validated Numerical Software For Algebraic Curves with Singularities
    Adrien Poteaux and Florent Bréhard - CRIStAL (Lille)
    
68. Bijections and counting of decorated planar maps
    Valentin Bonzom - LIGM, Université Gustave Eiffel
    
69. Monotonous multi-thread programming
    Dumitru Potop-Butucaru, Jean-Marie Madiot - INRIA Paris
    2-36-1
70. Incremental maintenance of queries on dynamic trees
    Antoine Amarilli, Charles Paperman, Inria Lille
    1-18
71. Enumerating simple paths satisfying a regular path query
    Antoine Amarilli, Mikaël Monet, Inria Lille
    
72. Compression of large dynamic graphs
    Binh-Minh Bui-Xuan and Mehdi Naima - Sorbonne Université, LIP6
    
73. Analyse automatisée de documents pour lutte contre la fraude documentaire F/H
    Guillaume Bernard - MAIF - Niort (g.bernard@maif.fr)
    
74. Anomaly Detection in Link Streams
    Maroua Bahri and Mehdi Naima
    
75. Inter-Model Explanations for Student Modeling in AI for Education
    marie-Jeanne Lesot & Sebastien Lalle - LIP6, Sorbonne University
    
76. Inria PhD track (internship + thesis): Computational Design of Evolving Porous Structures
    Jonàs Martínez and Sylvain Lefebvre
    https://recrutement.inria.fr/public/classic/fr/offres/2024-08348
77. Copoints enumeration in graph convexities
    Victor Chepoi, Oscar Defrain & Simon Vilmin, Aix-Marseille Université
    Graphes, combinatoire, complexité
78. Attaques sur Système de Distributions de Clés Quantiques (QKD)
    Laurent Maingault, Loïc MANGIN - CEA Grenoble
    2-34-2
79. Innovative Blockchain Internship Program at Nomadic Labs
    Yann Régis-Gianas, Head of Engineering - Paris, France
    
80. Optimisation interactive de programmes OCaml via des transformations source-à-source
    Arthur Charguéraud
    2.4,2.36.1,2.7.2
81. Implementation of cryptographic primitives on ML dedicated computational units
    Jean-Pierre Flori - Apple Europe, Paris
    
82. fine grain analysis of the implementations of classical algorithms and data structures in various contemporary programming languages
    Cyril Nicaud, Pablo Rotondo, LIGM, University Gustave Eiffel, Marne-la-Vallée
    2-10, 2-15
83. Coalition manipulability of IRV in Impartial Culture
    François Durand, Élie de Panafieu, Nokia Massy
    2-10, 2-15
84. Proving the equivalence of type and function definitions automatically in Coq
    Frédéric Blanqui - ENS Paris Saclay, Gif-sur-Yvette
    2-07-02,2-07-01
85. Stage de recherche en informatique : Reconnaissance de programmes par réseaux de neurones de graphes
    Sid Touati, Enrico Formenti, Christophe Alias
    
86. Bridging the gap between a verified library and a proof assistant
    Guillaume Melquiond - Laboratoire Méthodes Formelles, Université Paris Saclay, Inria
    2.7.2, 2.36.1
87. Vérification formelle des politiques de sécurité pour les protocoles IoT
    Quentin Peyras (IRIT) et Ghada Gharbi (Epita) - IRIT, Toulouse
    
88. Towards formally verified configuration languages
    Helene Coullon, Frederic Loulergue - IMT Atlantique Nantes France
    
89. Side-Channel Attacks on Elliptic Curve Cryptography
    Victor Lomné - Montpellier, France
    
90. Side-Channel Attacks on Post-Quantum Cryptography and Hybridation
    Thomas Roche - NinjaLab - Montpellier, France
    
91. Verification for the Varda distributed programming language
    Shapiro, Pagliari @LIP6 (Sorbonne-U, Jussieu)
    
92. A Kubernetes-based backend for the Varda distributed programming language
    Shapiro, Pagliari @LIP6 (Sorbonne-U, Jussieu)
    2.17, 2.18.1, 2.03, 1.31
93. Verification for the Varda distributed programming language
    Shapiro, Pagliari @LIP6 (Sorbonne-U, Jussieu)
    2.04, 2.18.1
94. Rigorous development of database backends
    Shapiro, @LIP6-Sorbonne-Université
    2.09.2, 2.26.1, 2.36.1, 2.18.1
95. Computer-Aided-Design of Zero-Waste Garment Patterns
    Adrien Bousseau, Inria Université Côte d'Azur
    
96. Optimisation des processus d'essai pour la validation des modèles dynamiques de véhicule
    Aubin - DGA
    
97. Ensuring Correctness in Open Systems through Compatibility
    R. Ameur-Boulifa (Sophia-Antipolis) et M. Ouerdini (Toulouse)M
    
98. Open Automata meet Session Types
    R. Ameur-Boulifa (Sophia) et L. Henrio (Lyon)
    
99. Multi-Agent Reinforcement Learning Implementation
    Benedikt Bollig, Matthias Fuegger, Thomas Nowak, Zhuofan Xu (ENS Paris-Saclay)
    
100. On-Line Parameter Estimation in Bioreactors
     Benedikt Bollig, Matthias Fuegger, Thomas Nowak, Mariapia D'Urso
     
101. Clock Discipline Algorithm in Coq
     Benjamin Lion, Inria centre de l'université de Rennes
     
102. Analyzing Mean Payoff Games Using Sums-of-Squares
     Mateusz Skomra - LAAS-CNRS (Toulouse)
     2.20.1
103. Robust clustering
     Michaël Poss - Montpellier (LIRMM)
     2.24.1
104. Traitement d’images spectrales de microscopie électronique assistée par IA appliqué à la classification de météorites.
     Guillaume Tochon (LRE EPITA) in partnership with Institut de Minéralogie, de Physique des Matériaux et de Cosmochimie (IMPMC)
     
105. Post-Quantum Threshold Signature Scheme from Code-based Assumptions
     Victor Dyseryn / Duong Hieu Phan - Télécom Paris
     2.12.2, 2.13.2
106. Improvement of a pipeline to enhance vascular structures in biomedical images
     Hugo Rositi - Loria, Nancy
     
107. https://webusers.i3s.unice.fr/~elozes/sujet-stage-printemps-ete-2025.pdf
     Diagrammes de séquences et modèles de cohérence faible
     
108. Diagrammes de séquences et modèles de cohérence faible
     Cinzia Di Giusto & Etienne Lozes
     
109. Scalable Translation Validation for High-Performance Computing and Machine Learning
     Christophe Alias - ENS de Lyon
     
110. Evaluation of complex queries on large knowledge bases
     Louis Jachiet - Télécom Paris
     2.26.1 2.26.2 2.29.2
111. Lower bounds on provenance and counting for recursive queries
     Antoine Amarilli
     
112. Graphical Conditions ensuring Equality between Differential and Mean Stochastic Dynamics
     François Fages, Inria Saclay, Ecole Polytechnique, Francois.Fages@inria.fr
     C2-19
113. Graphical Conditions ensuring EqGraphical display of biochemical reaction networks based on Petri Net invariants
     François Fages, Inria Saclay, Ecole Polytechnique, Francois.Fages@inria.fr
     C2-19
114. Modeling single-cell reaction networks with cell-cycle transition kernels
     Jakob Ruess, Inria Saclay, Jakob.Ruess@inria.fr
     2.19
115. Smoothed Analysis: Bridging Theory and Practice in Dynamic Networks
     Ami Paz. LISN: CNRS & Paris-Saclay University
     2-18-1 Algorithmique distribuée pour les reseaux
116. Distributed Dynamic Graph Algorithms
     Ami Paz. LISN: CNRS & Paris-Saclay University
     2-18-1 Algorithmique distribuée pour les reseaux
117. Development of algorithms for victim localization in disaster areas using a fleet of cooperative drones
     Marwane Rezzouki - Laboratoire des signaux et systèmes
     
118. Development of algorithms for victim localization in disaster areas using a fleet of cooperative drones
     Marwane Rezzouki - Laboratoire des signaux et systèmes
     
119. Auditing Practical Privacy Guarantees of Differentially Private Machine Learning Models
     Aurélien Bellet - Inria Montpellier
     Fondements de la confidentialité des données
120. Formalisation et vérification d’un UIDL formel bigraphique dans Coq (M2 + doctorat)
     Xavier Thirioux (ISAE-Supaero, Toulouse), Celia Picard (ENAC, Toulouse), Cyril Allignol (ENAC, Toulouse)
     
121. Data deformations preserving underlying model classes
     Adrien Hardy, QRT Zurich