Submit an internship offer

1. Formal Verification of Liveness in Distributed Systems via Reinforcement Learning
   Ocan Sankur, Florian Faissole (IRISA, Rennes)
   Related courses: ADVERIF, VCP
2. Cryptographic Simulator Synthesis Using Program Logics
   Adrien Koutsos, Aymeric Fromherz (Inria Paris)
   Related courses: SECURE, PROGPROOFS
3. Application of formal methods (Model Checking) for verifying Nuclear Power Plant Operating Procedures (possibility PhD CIFRE in 2026)
   Valentin RYCHKOV (EDF R&D Paris-Saclay)
   Related courses: SYNC, VCP, CTRLVERIF, ADVERIF
4. Decision Procedure for Equivalence Relations
   Pierre Corbineau and Lionel Rieg at Verimag, Grenoble INP - UGA, in Grenoble
   Related courses: Foundations of Proof Systems, Proof Assistants
5. WQO dichotomy for homogeneous structures (experimental evaluation)
   Slawomir Lasota, University of Warsaw
   Related courses: WQO
6. Kleene Algebra with Tests for probabilistic programs
   Patrick Baillot, Leandro Gomes (Lille, CRIStAL)
7. Reasoning on the execution time of programs with Kleene Algebra with Tests
   Patrick Baillot, Leandro Gomes (Lille, CRIStAL)
8. Variants of Higher-Dimensional Automata
   Uli Fahrenberg & Amazigh Amrane; location: LMF, ENS Paris-Saclay, 4 avenue des Sciences, 91190 Gif-sur-Yvette
9. Deep Learning Prediction of Enzyme Functions Beyond EC Classification
   François Coste, Centre Inria de l’Université de Rennes
10. Dolev-Yao-Model-Guided Fuzzing of E-Voting Protocols
    Lucca Hirschi, Inria Nancy, France
    Related courses: SECURE
11. Optimising MBQC Patterns
    Maxime Garnier and Thierry Martinez, QAT, Inria/DIENS
    Related courses: QUANTUM, QALCO, APPROX, HEU
12. Formalising MBQC in Rocq
    Maxime Garnier and Thierry Martinez, QAT, Inria/DIENS
    Related courses: QUANTUM, QALCO, PRFA, PROGPROOFS
13. Locally Private Compression: Low-Complexity at Finite Blocklengths
    Aslan Tchamkerten
14. Drawing toroidal 3-connected graphs, via Schnyder woods
    Luca Castelli Aleardi (LIX, Ecole Poytechnique)
    Related courses: GEOMGRAPHS
15. Chiffrement avancé fondé sur les problèmes LWE
    Thomas Ricosset - Thales Gennevilliers
    Related courses: LCRYPT
16. Cryptanalyse symétrique aidée par MILP
    Nicolas David - Thales Gennevilliers
    Related courses: CODES
17. Computational Differential Algebra for the Enumeration of Regular Bipartite Graphs
    Frédéric Chyzak, Inria Saclay (in Palaiseau)
    Related courses: COMPALG, COMBIAA, AOFA
18. Conditional reasoning for mechanised cryptographic proofs
    Joseph Lallemand & David Baelde, équipe SPICY, IRISA, Rennes
    Related courses: SECURE
19. Intégration des approches topologiques et géométriques dans le cadre de la modélisation 3D
    Bac Alexandra, Aldo Gonzalez-Lorenzo, Yann-Situ Gazull (LIS Marseille)
    Related courses: Computational Geometry and Topology, Algorithms and Combinatorics of Geometric Graphs
20. Modélisation formelle des algorithmes de protection lanceur
    Danko Ilik, CNES Paris-Daumesnil
    Related courses: PRFA, CGT, COMPALG
21. Circuit Complexity, Reaction Networks, and Analog Computations.
    Olivier Bournez, LIX, Ecole Polytechnique
22. Various topics in proof assistants, programming languages, and logic
    Yannick Forster, Inria Paris, Team Cambium
    Related courses: PRFA, PRFSYS, PROGPROOFS, FUN, SEMPL, ECOLO, SECURE, HOTT
23. Source-to-source Transformations of Coq/Rocq Proof Scripts: Removing, Inlining, Expanding Tactics
    Nicolas MAGAUD
    Related courses: Logic/Proof
24. A formal study of finite projective planes using Rocq
    Nicolas MAGAUD (ICube UMR 7357 CNRS-Université de Strasbourg)
    Related courses: Logic/Proof
25. Automatic proofs in projective geometry : finite projective spaces, spreads, and packings
    Nicolas MAGAUD (ICube UMR 7357 CNRS-Université de Strasbourg)
    Related courses: Logic/Proof
26. Probabilities of Regular Languages of Infinite Trees
    Paweł Parys, University of Warsaw, Poland
27. Local extensions of type theory
    Théo Winterhalter, ENS Paris-Saclay
    Related courses: PRFA, PRFSYS, PROGPROOFS, FUN, SEMPL, ECOLO, SECURE, HOTT
28. Improving the memory footprint of MPCitH
    Rafael del Pino & Morgane Guerreau, PQShield (Paris)
29. Neural Network Architectures for Second Order Side Channel Attacks
    Timo Zijlstra, PQShield SAS (Paris)
30. Gamess with Boolean Combinations of Energy and Parity Objectives
    Aditya Prakash and Karoliina Lehtinen, LIS, Aix-Marseille Université
    Related courses: The intern would benefit from ADVERIF or JEUXSTO but it is not necessary.
31. Circuit equational theories with control and ancillas
    Chris Heunen, Louis Lemonnier at Quantum Software Lab, University of Edinburgh
    Related courses: QUANTUM, SEMPL
32. Transition Post-Quantique d'un Protocole VPN
    Sylvain Ruhault, Abdel Rahman Taleb (ANSSI, Paris)
33. Transition Post-Quantique des Protocoles de Vote Électronique : Hybridation et Sécurité
    Sylvain Ruhault, Abdel Rahman Taleb (ANSSI, Paris)
34. Approximating the safety value in partially observable Markov decision processes
    Thomas Brihaye & Pierre Vandenhove, Université de Mons (Belgium)
    Related courses: JEUXSTO, ADVERIF
35. From Theory to Performance: Building Efficient Reasoners for Standpoint Logic
    Lucía Gómez Álvarez, at the Inria Centre at the University Grenoble Alpes
36. Modelling Multi-Perspective Knowledge on the Semantic Web
    Lucía Gómez Álvarez, at the Inria Centre at the University Grenoble Alpes
37. A formally verified equational theory of modern regular expressions
    Supervisors: Aurèle Barrière, Clément Pit-Claudel and Gabriel Radanne. Location: Lyon, France.
38. Open Automata meet Choreographies
    Rabéa Ameur-Boulifa, Cinzia Di Giusto and Ludovic Henrio: Internship in Sophia Antipolis Eurecom and Lab I3S
39. Développement d’une architecture de contrôle de la pose 2D d'un robot non-holonome par l’apprentissage par renforcement incluant la gestion de manœuvres et l’évitement d’obstacles
    Mélodie DANIEL - Laboratoire Bordelais de Recherche en Informatique (LaBRI) Bordeaux, France
40. Développement d’une architecture de contrôle en corps complet par apprentissage par renforcement pour la manipulation d’objets articulés distants
    Mélodie DANIEL et Olivier LY - Laboratoire Bordelais de Recherche en Informatique (LaBRI) Bordeaux, France
41. Perception multi-sensorielle et suivi temporel d’objets déformables pour la robotique agricole autonome
    Mélodie DANIEL et Olivier LY - Laboratoire Bordelais de Recherche en Informatique (LaBRI) Bordeaux, France
42. Cooperation and Competition in Online Markets
    Felipe Garrido-Lucero, Université Toulouse Capitole, Toulouse, France
    Related courses: Probability and Algorithmic Applications, Algorithms for Stochastic Games
43. Encoding type systems with universes in Dedukti
    Frédéric Blanqui, ENS Paris Saclay
    Related courses: prfsys, prfa, 1-33, fun
44. Translating Rocq or Lean proofs to Isabelle/HOL
    Frédéric Blanqui, ENS Paris Saclay
    Related courses: prfsys, prfa, 1-33, fun
45. Method Combinations for Programming Languages with Multiple Dispatch
    Didier Verna, EPITA Research Lab, 14-16 rue Voltaire, 94270 Le Kremlin-Bicêtre
46. Mathematical Investigation of Non-Deterministic Switches in Cell Regulation
    Stefan HAAR, MUSCA Team, INRIA Saclay, Bât. Turing, Palaiseau
47. Soundness of Rust Verification in the Presence of Safe and Unsafe Code
    Yannick Zakowski at Inria Paris in the Cambium Research Group. Co-advised remotely by Son Ho, designer of Aeneas.
48. Boolean Complexity for Validated Numerical Resolution of Algebraic Curve Singularities
    Adrien Poteaux, Rémi Prébet and Florent Bréhard - CRIStAL, Univ. Lille
    Related courses: COMPALG
49. Combinatorial and computational properties of hom shifts
    Benjamin Hellouin de Menibus ; LISN, université Paris-Saclay
    Related courses: Symbolic Dynamics, Algorithmic Aspects of Combinatorics
50. Model Checking for Open Automata
    Rabéa Ameur-Boulifa (Télécom Paris – Sophia Antipolis) and Ludovic Henrio (ENS Lyon)
    Related courses: Foundations of Proof Systems
51. Singular Euler-Maclaurin Expansion in Rocq
    Andreas Buchheit, Cyril Cohen (Inria Lyon), Dominik Kirst (Inria Paris), Assia Mahboubi (Inria Rennes, Nantes site)
    Related courses: Proof assistants
52. Learning Tree Automata
    Adrien Pommellet & Amazigh Amrane - Location : EPITA Paris, LRE, 14-16 Rue Voltaire, 94270 Le Kremlin-Bicêtre
53. Typst
    Gabriel Scherer, Paris
    Related courses: Functional programming and Type Systems (FUN)
54. Comparing large genomic datasets with Invertible Bloom Lookup Tables
    Gregory Kucherov
    Related courses: PROBAS, AOFA, CODES
55. Intersection Types for the Positive Lambda Calculus
    Delia Kesner and Giulio Manzonetto (IRIF, Universite Paris Cite)
56. Parallel Abstract Interpretation
    Valentin Perrelle, CEA List (Palaiseau)
    Related courses: AISAV
57. Program representations for Deep Learning
    Michele Alberti, Valentin Perrelle, CEA List (Palaiseau)
58. Méthodes symboliques pour la bi-déduction dans le contexte de la vérification de protocoles de sécurité
    David Baelde et Stéphanie Delaune
    Related courses: SECURE
59. Conception d’un langage de propriétés pour les protocoles cryptographiques en Squirrel
    David Baelde et Stéphanie Delaune (Équipe Spicy, IRISA, Rennes)
    Related courses: SECURE
60. Verifying security protocols with exclusive-or using PROVERIF
    Vincent Cheval (Oxford UK) et Stéphanie Delaune, Équipe Spicy, IRISA, Rennes
    Related courses: SECURE
61. Canonical for Rocq
    Pierre Boutry, Chase Norman, Loïc Pujet. In Strasbourg University.
    Related courses: PRFA, PRFSYS, HOTT
62. A syntax for proof-relevant Observational Type Theory
    Loïc Pujet. In Strasbourg University.
    Related courses: PRFA, PRFSYS, HOTT, SEMPL
63. Side-Channel Analysis of a post-quantum encryption scheme without re-encryption
    Gabriel Zaid and Mélissa Rossi
    Related courses: LCRYPT, CODES
64. Post-Quantum Anonymous Credentials
    Matthieu Rivain and Thibauld Feneuil
    Related courses: LCRYPT, SECURE, FIP
65. The Künneth theorem in Homotopy Type Theory
    Pierre Boutry, Viktoria Heu, Loïc Pujet. In Strasbourg University.
    Related courses: PRFA, PRFSYS, HOTT, SEMPL, CGT
66. Code de Gray: délai et espace constant
    Victor Marsault et Yann Strozecki, LIGM (Université Gustave Eiffel)l
67. Étude des automates à deque
    Victor Marsault et Yann Strozecki, LIGM (Université Gustave Eiffel)l
68. Model-Checking Linear Dynamical Systems under Floating Point Rounding
    Engel Lefaucheux, Inria Nancy
    Related courses: ADVERIF, CTRLVERIF, WQO
69. Anamorphic Cryptography
    Hieu Phan
70. Model-Checking Techniques for Virus and Malware Detection
    Tayssir Touili (IRIF)
    Related courses: adverif,vcp,aisav
71. Gradual and Semantic Typing for Elixir's Module System (2 internship subjects)
    Giuseppe Castagna (IRIF, Paris) in collaboration with the Elixir development team
    Related courses: Functional Programming and Type Systems
72. Extending Polymorphic Type Inference for Dynamic Languages: Gradual Typing and Efficient Implementation (2 internship subjects)
    Giuseppe Castagna (IRIF, Paris) and Kim Nguyen (LMF, Paris Saclay)
    Related courses: Functional Programming and Type Systems
73. vanced Typing of Map Data Structures in Elixir (3 internship subjects)
    Giuseppe Castagna (IRIF, Paris) in collaboration with the Elixir development team
    Related courses: Functional Programming and Type Systems