Internships 2025-2026
- Formal Verification of Liveness in Distributed Systems via Reinforcement Learning
Ocan Sankur, Florian Faissole (IRISA, Rennes)
Related courses: ADVERIF, VCP - Cryptographic Simulator Synthesis Using Program Logics
Adrien Koutsos, Aymeric Fromherz (Inria Paris)
Related courses: SECURE, PROGPROOFS - 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 - 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 - WQO dichotomy for homogeneous structures (experimental evaluation)
Slawomir Lasota, University of Warsaw
Related courses: WQO - Kleene Algebra with Tests for probabilistic programs
Patrick Baillot, Leandro Gomes (Lille, CRIStAL) - Reasoning on the execution time of programs with Kleene Algebra with Tests
Patrick Baillot, Leandro Gomes (Lille, CRIStAL) - Variants of Higher-Dimensional Automata
Uli Fahrenberg & Amazigh Amrane; location: LMF, ENS Paris-Saclay, 4 avenue des Sciences, 91190 Gif-sur-Yvette - Deep Learning Prediction of Enzyme Functions Beyond EC Classification
François Coste, Centre Inria de l’Université de Rennes - Dolev-Yao-Model-Guided Fuzzing of E-Voting Protocols
Lucca Hirschi, Inria Nancy, France
Related courses: SECURE - Optimising MBQC Patterns
Maxime Garnier and Thierry Martinez, QAT, Inria/DIENS
Related courses: QUANTUM, QALCO, APPROX, HEU - Formalising MBQC in Rocq
Maxime Garnier and Thierry Martinez, QAT, Inria/DIENS
Related courses: QUANTUM, QALCO, PRFA, PROGPROOFS - Drawing toroidal 3-connected graphs, via Schnyder woods
Luca Castelli Aleardi (LIX, Ecole Poytechnique)
Related courses: GEOMGRAPHS - Chiffrement avancé fondé sur les problèmes LWE
Thomas Ricosset - Thales Gennevilliers
Related courses: LCRYPT - Computational Differential Algebra for the Enumeration of Regular Bipartite Graphs
Frédéric Chyzak, Inria Saclay (in Palaiseau)
Related courses: COMPALG, COMBIAA, AOFA - Conditional reasoning for mechanised cryptographic proofs
Joseph Lallemand & David Baelde, équipe SPICY, IRISA, Rennes
Related courses: SECURE - 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 - Modélisation formelle des algorithmes de protection lanceur
Danko Ilik, CNES Paris-Daumesnil
Related courses: PRFA, CGT, COMPALG - Circuit Complexity, Reaction Networks, and Analog Computations.
Olivier Bournez, LIX, Ecole Polytechnique - 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 - Source-to-source Transformations of Coq/Rocq Proof Scripts: Removing, Inlining, Expanding Tactics
Nicolas MAGAUD
Related courses: Logic/Proof - A formal study of finite projective planes using Rocq
Nicolas MAGAUD (ICube UMR 7357 CNRS-Université de Strasbourg)
Related courses: Logic/Proof - Automatic proofs in projective geometry : finite projective spaces, spreads, and packings
Nicolas MAGAUD (ICube UMR 7357 CNRS-Université de Strasbourg)
Related courses: Logic/Proof - Local extensions of type theory
Théo Winterhalter, ENS Paris-Saclay
Related courses: PRFA, PRFSYS, PROGPROOFS, FUN, SEMPL, ECOLO, SECURE, HOTT - Neural Network Architectures for Second Order Side Channel Attacks
Timo Zijlstra, PQShield SAS (Paris) - 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. - Circuit equational theories with control and ancillas
Chris Heunen, Louis Lemonnier at Quantum Software Lab, University of Edinburgh
Related courses: QUANTUM, SEMPL - Transition Post-Quantique des Protocoles de Vote Électronique : Hybridation et Sécurité
Sylvain Ruhault, Abdel Rahman Taleb (ANSSI, Paris) - Approximating the safety value in partially observable Markov decision processes
Thomas Brihaye & Pierre Vandenhove, Université de Mons (Belgium)
Related courses: JEUXSTO, ADVERIF - From Theory to Performance: Building Efficient Reasoners for Standpoint Logic
Lucía Gómez Álvarez, at the Inria Centre at the University Grenoble Alpes - Modelling Multi-Perspective Knowledge on the Semantic Web
Lucía Gómez Álvarez, at the Inria Centre at the University Grenoble Alpes - A formally verified equational theory of modern regular expressions
Supervisors: Aurèle Barrière, Clément Pit-Claudel and Gabriel Radanne. Location: Lyon, France. - Open Automata meet Choreographies
Rabéa Ameur-Boulifa, Cinzia Di Giusto and Ludovic Henrio: Internship in Sophia Antipolis Eurecom and Lab I3S - 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 - 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 - 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 - Cooperation and Competition in Online Markets
Felipe Garrido-Lucero, Université Toulouse Capitole, Toulouse, France
Related courses: Probability and Algorithmic Applications, Algorithms for Stochastic Games - Encoding type systems with universes in Dedukti
Frédéric Blanqui, ENS Paris Saclay
Related courses: PRFSYS, PRFA, FUN - Translating Rocq or Lean proofs to Isabelle/HOL
Frédéric Blanqui, ENS Paris Saclay
Related courses: PRFSYS, PRFA, FUN - Method Combinations for Programming Languages with Multiple Dispatch
Didier Verna, EPITA Research Lab, 14-16 rue Voltaire, 94270 Le Kremlin-Bicêtre - Mathematical Investigation of Non-Deterministic Switches in Cell Regulation
Stefan HAAR, MUSCA Team, INRIA Saclay, Bât. Turing, Palaiseau - 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. - 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 - Combinatorial and computational properties of hom shifts
Benjamin Hellouin de Menibus ; LISN, université Paris-Saclay
Related courses: Symbolic Dynamics, Algorithmic Aspects of Combinatorics - 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 - 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 - Learning Tree Automata
Adrien Pommellet & Amazigh Amrane - Location : EPITA Paris, LRE, 14-16 Rue Voltaire, 94270 Le Kremlin-Bicêtre - Comparing large genomic datasets with Invertible Bloom Lookup Tables
Gregory Kucherov
Related courses: PROBAS, AOFA, CODES - Intersection Types for the Positive Lambda Calculus
Delia Kesner and Giulio Manzonetto (IRIF, Universite Paris Cite) - 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 - 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 - Verifying security protocols with exclusive-or using PROVERIF
Vincent Cheval (Oxford UK) et Stéphanie Delaune, Équipe Spicy, IRISA, Rennes
Related courses: SECURE - Canonical for Rocq
Pierre Boutry, Chase Norman, Loïc Pujet. In Strasbourg University.
Related courses: PRFA, PRFSYS, HOTT - A syntax for proof-relevant Observational Type Theory
Loïc Pujet. In Strasbourg University.
Related courses: PRFA, PRFSYS, HOTT, SEMPL - Side-Channel Analysis of a post-quantum encryption scheme without re-encryption
Gabriel Zaid and Mélissa Rossi
Related courses: LCRYPT, CODES - Post-Quantum Anonymous Credentials
Matthieu Rivain and Thibauld Feneuil
Related courses: LCRYPT, SECURE, FIP - 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 - Code de Gray: délai et espace constant
Victor Marsault et Yann Strozecki, LIGM (Université Gustave Eiffel)l - Model-Checking Linear Dynamical Systems under Floating Point Rounding
Engel Lefaucheux, Inria Nancy
Related courses: ADVERIF, CTRLVERIF, WQO - Model-Checking Techniques for Virus and Malware Detection
Tayssir Touili (IRIF)
Related courses: ADVERIF, VCP, AISAV - 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 - 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 - Advanced 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 - Certified compilation of concurrent programs
Jean-Marie Madiot, Inria Paris
Related courses: PRFSYS, PROGPROOFS - Formally Secure Compilation Against Spectre Attacks
Catalin Hritcu, MPI-SP, Bochum, Germany
Related courses: FUN, PRFSYS, PRFA, SECURE, SYNC, PROGPROOF - Sporadic tasks in uniprocessor fixed-priority scheduling with non-resumable starting and resuming delays
Hadrien Barral, LIGM, Université Gustave Eiffel - Finding points of interests for complex faults injection models
Hadrien Barral, LIGM, Université Gustave Eiffel - Secret quorums protecting byzantine reliable broadcast against adaptive adversaries
Maxence Perion and Sara Tucci, Universite Paris-Saclay, CEA (Palaiseau)
Related courses: PODC, DISC, CRYPTALG, SECURE - Smoothed Analysis: Bridging Theory and Practice in Dynamic Networks
Ami PAZ, Paris-Saclay University
Related courses: DISC, PODC - Solving Differential Equations in Rocq
Florent Bréhard (CRIStAL, Univ Lille), Damien Pous, Nicolas Brisebarre (LIP, ENS Lyon)
Related courses: PRFA, COMPALG - Algorithms in Computer Assisted Proofs for Ordinary Differential Equations
Florent Bréhard (CRIStAL, Univ Lille), Nicolas Brisebarre, Rémi Prébet (LIP, ENS Lyon), Maxime Breden (CMAP, École Polytechnique)
Related courses: COMPALG, AISAV - Relational Separation Logic for Compiler Verification
Xavier Leroy and François Pottier, Inria Paris
Related courses: FUN, PROGPROOFS, PRFA - Certified Symbolic-Numeric Algorithms for Connectivity on semi-algebraic sets
Rémi Prébet (LIP, ENS Lyon), Florent Bréhard and Nicolas Brisebarre
Related courses: COMPALG, AISAV - Interactive Program Verification Meets Abstract Interpretation
Aymeric Fromherz (Prosecco team, Inria Paris). Co-advised by Benoit Montagu (Epicure Team, Irisa) and Son Ho (Microsoft Azure Research, Cambridge, UK)
Related courses: AISAV, FUN, PROGPROOFS - F* proof-oriented programming language
Catalin Hritcu, MPI-SP, Bochum, Germany
Related courses: FUN, PRFSYS, PRFA, SECURE, PROGPROOFS - Vérification formelle des politiques de sécurité pour les protocoles IoT
Quentin Peyras, IRIT, Toulouse - Large-Scale Seismic Imaging: Distributed Reverse Time Migration Accelerated by AI
Wilfried Kirschenmann - Boulogne-Billancourt (France) - Computation of distances between transducer models and application to approximate learning of word functions and relations
Benjamin Monmege, Marseille (Aix-Marseille Université, Laboratoire d'Informatique et des Systèmes)
Related courses: MATA, VCP, ADVERIF - An NLP framework to automatically evaluate the adequacy and relevance of assessment items
Luca Benedetto, Telecom SudParis (IP Paris) - Exploring interactions between automated program analysis and witnesses
Raphaël Monat, Inria Lille
Related courses: AISAV - Experimental evaluation of relational abstract domains
Raphaël Monat, Inria Lille
Related courses: AISAV - Model Checking for Open Automata
Rabéa Ameur-Boulifa (Télécom Paris – Sophia Antipolis) and Ludovic Henrio (ENS Lyon)
Related courses: VCP, ADVERIF, CTRLVERIF - M2 internship (ENS-PSL & Inria Paris) related to logic-based methods for AI and databases
Michaël Thomazo and Meghyn Bienvnu, ENS-PSL, Inria
Related courses: QD - Réseaux booléens degré-bornés
Adrien Richard - I3S (UMR CNRS 7271) - Sophia Antipolis (Nice)
Related courses: MATA - Graphe d’interaction, propriétés dynamiques, et complexité des réseaux booléens
Adrien Richard - I3S (UMR CNRS 7271) - Sophia Antipolis (Nice)
Related courses: MATA - COMPLB - Synchronisation des réseaux booléens asynchrones
Adrien Richard - I3S (UMR CNRS 7271) - Sophia Antipolis (Nice)
Related courses: MATA - Translation of formal proofs between set theory encodings
Catherine Dubois, Thomas Traversié - Paris-Saclay ou Evry - Formally Verified Compilation of an Interaction-Oriented Programming Language
Cyril Allignol, Basile Pesin and Celia Picard; Ecole Nationale de l'Aviation Civile (Toulouse) - M2 Internship Opportunity - Concurrent Autonomic Control for the Computing Continuum
Farah AIT SALAHT (ESILV/DVRC) and Christian Perez (Inria/ENS Lyon). Internship Location: Research Center of the Léonard de Vinci Pôle Universitaire, 92916 Paris La Défense, France. - Inference of Broadcast protocols
Peter Habermehl and Tali Sznajder (IRIF, Paris)
Related courses: MATA