Internships 2023/2024
Submit an internship offer
Optimal stopping theory with predictions
Spyros Angelopoulos and Christoph Dürr, LIP6-Sorbonne University
2.24.1, 2.11
Formal Methods for the Verification of Self-Adapting Distributed Systems
Radu Iosif & Arnaud Sangnier - Location : Verimag
2.8 2.9.2 2.18.2
Schnyder woods for higher genus surfaces, with applications to graph drawing
Luca Castelli Aleardi - Ecole Polytechnique (LIX)
2.38.1
Formal verification for quantum programming
Christophe Chareton and Nicolas Blanco, CEA LIST, Paris-Saclay
2.34 - 2.36.1 - 2.7 - 2.4
Consommation de ressources par les programmes réactifs fonctionnels
Jules Chouquet - LIFO, Orléans
Programming Abstract Machines and Multi Types
Beniamino Accatoli & Gabriele Vanoni - LIX & IRIF - Paris
2.1, 2.2, 2.4
Modeling the Interaction Between Microalgae and Bacteria
Matthias Függer, Thomas Nowak (ENS Paris-Saclay)
Formal Rules for Plasmid Design
Benedikt Bollig, Matthias Függer, Thomas Nowak (ENS Paris-Saclay)
How Many Growth Curves are Enough?
Matthias Függer, Thomas Nowak (ENS Paris-Saclay)
Symmetric Neural Networks for Symmetric Problems
Benedikt Bollig, Matthias Függer, Thomas Nowak (ENS Paris-Saclay)
Clique of tournaments
Pierre Aboulker
Advanced graph theory, Parametrized complexity,
Efficient algorithms for enumeration problems in graphs
Pierre Bergé and Vincent Limouzy - Université Clermont Auvergne
Parameterized complexity, Algorithms and combinatorics for geometric graphs, Advanced graph theory
Semantics of inductive types
Ambroise Lafont - Ecole Polytechnique (LIX)
Internship subject (Master 2 or Master 1) Open Automata meet Session Types
Rabéa Ameur-Boulifa and Ludovic Henrio - Sophia Antipolis
Automata and Formal Languages, Logics and Semantics of Programs
Open Automata meet Session Types
Rabéa Ameur-Boulifa (Teelecom Paris) and Ludovic Henrio (ENS) - Sophia Antipolis
Automata and Formal Languages, Logics and Semantics of Programs
Bowyer-Watson Algorithm for Delaunay Triangulation on Hyperbolic Surfaces
Vincent Despré & Marc Pouget
2.14.1 Computational geometry and topology, 2.38.1 Algorithms and combinatorics for geometric graphs
Formal explanations for trustworthy explainable AI
Julien Girard-Satabin / CEA Saclay
Variable substitution for efficient formal verification of Neural Networks
François Bobot, CEA LIST, Université Paris-Saclay
Polynomial zonotopes for neural network verification
Augustin Lemesle, CEA LIST, Université Paris-Saclay
A diagram editor to help mechanise categorical proofs in Coq
Ambroise Lafont - Ecole Polytechnique
Behavioural Distances for Higher-Order Languages with Continuous Probabilities
Raphaëlle Crubillé, LIS (Marseille)
Langages de programmation probabilistes
Towards Formal Semantics and Proven Compliance of Business Workflows Processing Personal Data
Vincent Hugot – LIFO / INSA CVL
Smoothed Analysis of Dynamic Networks
Ami Paz: LISN, CNRS & Paris Saclay University
2-18-1 Algorithmique distribuée pour les réseaux
Distributed Dynamic Graph Algorithms
Ami Paz: LISN, CNRS & Paris Saclay University
2-18-1 Algorithmique distribuée pour les réseaux
Call-by-Need Models
Giulio Manzonetto & Beniamino Accattoli - IRIF & Inria Saclay
Lambda calculus, functional languages, denotational semantics — modules 2.1, 2.2, 2.4
A Generalized Search Command for Coq-Actema
B. Werner; Inria-LIX
2-7-1 2-7-2
Outputting Actema Proofs
B. Werner; Inria-LIX
2-7-1 2-7-2
Arbres de défaillances et formes normales exp-log
Danko Ilik - CNES Direction du transport spatial
Secure Implementation of Post-Quantum Signatures based on Multiparty Computation
Matthieu Rivain - CryptoExperts, Paris
2.12, 2.13, 2.34
Study and Improvement of Recent (Zero-Knowledge) Proof Systems
Matthieu Rivain - CryptoExperts, Paris
2.12, 2.13, 2.34
Distributed Graph Coloring Revisited
Ami Paz: LISN, CNRS & Paris-Saclay University
Algorithmique distribuée pour les reseaux
Nested Inference for Reactive Probabilistic Programming
Guillaume Baudart - ENS
Langages de programmation probabilistes
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
Reasoning on the execution time of programs with Kleene Algebra with Tests
Patrick Baillot (CRIStAL, Lille)
Languages of Higher Dimensional Automata
Emily Clement et Jérémy Ledent
Concurrency (2.3.1)
Ghost dependent types
Théo Winterhalter — ENS Paris Saclay
2.7.1, 2.7.2
A monadic approach to differentiation
Marie Kerjean - LIPN
2.1, 2.2, 2.4
Efficient computations of contiguity matrices for statistics and physics
Jérémy Berthomieu - LIP6, Sorbonne Université
2.13.1 2.22
Efficient computations of contiguity matrices for statistics and physics
Jérémy Berthomieu - LIP6, Sorbonne Université
2.13.1 2.22
Deep Neural Networks for Multimodal Expression Recognition in eHealth Applications
Eric Granger, Montréal, Canada
Introduction to Computer Vision, Logical aspects of artificial intelligence,Structures informatiques et logiques pour la modélisation linguistique,
Various topics in formal logic and proof assistants
Yannick Forster, Inria Paris
2-7-1, 2-7-2
Characterization of complexity and computability classes with Ordinary Differential Equations Continuous time Analog machines and models of computation.
Olivier Bournez
Complexity theory with Discrete Differential Equations/Finite differences.
Olivier Bournez
Programming with Ordinary Differential Equations and Continuous Time: Towards a programming language or pseudo-programming language.
Olivier Bournez
Computability and Complexity Theory for Models of Very Deep Learning.
Olivier Bournez
LLMs pour l’optimisation prédictive de la supply chain
Victor Nicollet - Lokad, 83-85 boulevard Vincent Auriol Paris 13
Typing Behaviors for Elixir
Giuseppe Castagna (IRIF), José Valim (Dashbit, Elixir)
2.4
Filtering for interactive systems
Géry Casiez, Mathieu Nancel, Daniel Vogel
Improvement of graph-based algorithms for image analysis
Julien Baste, Deise Santana Maia - CRIStAL, université de Lille
Efficient algorithms for video shot detection
Julien Baste, Deise Santana Maia - CRIStAL, université de Lille
Semi-Decentralized Federated Learning
Giovanni Neglia
Quantum Distributed Computing
Marc-Olivier Renou - Inria Saclay Polytechnique
2.18.1 and 2.34.1
Plane projection of a smooth curve
Guillaume Moroz, Marc Pouget - LORIA - Nancy
2.14.1 Computational geometry and topology. 2.24.2 Solving optimization problems with search heuristics.
Conditioning of the Roots of a Random Polynomial
Guillaume Moroz - LORIA - Nancy
2.24.2 Solving optimization problems with search heuristics. 2.11/2.11.2 Randomness in complexity.
Type-based security properties assurance in the Rust-based Redox operating system
Louis Rilling and Frédéric Tronel - IRISA/CentraleSupélec Rennes
Casser des Graphes
Matthieu Latapy, LIP6, Jussieu, Paris
Perturbations du Trafic Maritime par des Mouvements Sociaux
Matthieu Latapy, LIP6, Jussieu, Paris
Incremental maintenance of queries on dynamic trees
Antoine Amarilli, Charles Paperman, Télécom Paris or Université de Lille
Probabilistic uncertainties and analysis of quantum programs
Eric Goubault and Sylvie Putot, LIX, Ecole Polytechnique
Probabilistic properties and AI safety
Eric Goubault and Sylvie Putot, LIX, Ecole Polytechnique
Computability over partially ordered sets
Mathieu Hoyrup, Loria, Nancy
2.2, 2.33.3
Descriptive complexity of topological invariants
Mathieu Hoyrup, Loria, Nancy
2.33.3
Computing p-Centers and p-Medians through Maximum Satisfiability
Sami Cherif - MIS UR 4290, Université de Picardie Jules-Verne, Amiens
Logical Aspects of Artificial Intelligence, Combinatorial Optimization
Modular Analysis for Formal Verification of Integrated Circuits at Transistor Level
Matthieu Moy, Bruno Ferres, Pascal Raymond - Lyon or Grenoble
Impact environnemental du numérique : étudier le passé pour anticiper le futur ?
Matthieu Moy
Décroissance numérique : quels écosystèmes logiciels pour l’informatique écoresponsable ?
Matthieu Moy, Guillaume Salagnac, Lionel Morel, Michael Rao
Studying lattice problems for cryptography
Alice Pellet-Mary (Université de Bordeaux)
2.12.1, 2.12.2, 2.34.2
Vers un interpréteur abstrait produisant des preuves de correction
Benoit Montagu, Thomas Jensen, equipe Epicure, Inria Rennes
2.4, 2.6, 2.7.1, 2.7.2
Formalizing Hardware Security Mechanisms: a new HDL for modular hardware proofs
Pierre Wilke - CentraleSupélec Rennes
Formalizing RISC-V Enclaves
Pierre Wilke - CentraleSupélec Rennes
Formalizing Hardware Security Mechanisms: interrupts, MMU and SMT proofs
Pierre Wilke - CentraleSupélec Rennes
Modélisation formelle de systèmes multi-agents cyber-physiques communicants – Analyse et preuves de propriétés
Prof. Burkhart Wolff (LMF), Paolo Crisafulli (IRT SystemX) - IRT SystemX, Palaiseau
Proof assistants, Proof of Programs, Concurrency
Reachability Analysis of Infinite Markov Chain
Alain Finkel, Serge Haddad, Lina Ye - LMF
Verification of equivalence-based properties - beyond diff-equivalence
Stéphanie Delaune & Joseph Lallemand - Irisa, Rennes
2.30
Plusieurs sujets IA (texte/son/image) à l'INA
Nicolas Hervé - Bry-sur-Marne
Algorithme de reconstruction d’une forme continue à partir d’un objet discret
Étienne Baudrier, Étienne Le Quentrec - équipe IMAGeS, laboratoire iCube, Illkirch, université de Strasbourg
Algorithmes pour la lecture automatique de cernes et l’interdatation sur plusieurs espèces de chênes
Marion Jourdan (SILVA), Isabelle Debled-Renesson et Phuc Ngo (LORIA) - LORIA, Vandœuvre-lès-Nancy
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
How to make a temporal graph connected?
Thomas Bellitto, Bruno Escoffier - LIP6, Sorbonne Université
DNA Computing and DNA nanotechnology
Damien Woods, Hamilton Institute, Maynooth University, Ireland
Algorithms and Complexity modules
A Balancing Act with Numerics and Computer-Aided Proofs (the case study of Equilibrium Measures)
Mioara Joldes – LAAS-CNRS, Toulouse
Génération d’invariants de programmes par un grand modèle de langage
Simon Robillard, Maximos Skandalis (LIRMM)
Compositional reasoning for asynchronous message-passing software
Giovanni Bernardi
Zero-Knowledge proofs and applications (thresholdsignatures, confidential transactions, secure data management etc.)
Pierre-Alain Fouque (Rennes & IUF), Matthieu Rambaud & Weiqiang Wen (Télécom Paris)
Query-Directed Width Measures for Probabilistic Graph Homomorphisms
Antoine Amarilli, Mikaël Monet, Inria Lille
Chemins dans les graphes temporels avec futur incertain
Michael Raskin et Nicolas Hanusse — LaBRI,Talence, Bordeaux Métropole
SECOMP: Formally Secure Compilation of Compartmentalized C Programs
Catalin Hritcu, MPI-SP, Bochum, Germany
2.7.2, 2.7.1, 2.30, 2.4
Passive Learning of Symbolic Automata
Peter Habermehl - IRIF (CNRS, Université Paris Cité)
2-16
Raisonnement interactif pour les systèmes de contrôle embarqués
Timothy Bourke et Marc Pouzet
2-23-1
How smooth is a signal? A Type System for Discrete and Continuous-time Signals for Zélus
Marc Pouzet et Timothy Bourke
2-23-1
Hybrid System Models with Transparent Assertions
Marc Pouzet et Timothy Bourke - ENS/Inria Paris
2-23-1
Towards a Nonlinear Bound of Mutual Information Leakage for Additive-Masked Implementations
Olivier Rioul, Télécom Paris
Understanding Perceived Information and Hypothetical Information for Side-Channel Attacks
Olivier Rioul, Télécom Paris
Study of artificial intelligence algorithms with information theory via the information-bottleneck framework
Olivier Rioul, Télécom Paris
https://perso.telecom-paristech.fr/rioul/stage3.pdf
Implementation of hierarchies of algebraic structures in type theory
Assia Mahboubi – Nantes
Refinement Types for Liveness Properties in Denotational Semantics
Colin RIBA (LIP – ÉNS de Lyon
2.2, 2.4, 2.8
Operation research for arithmetic problems
Florent de Dinechin and Anastasia Volkova - CITI laboratory (INSA Lyon/Inria)
Compl ́etude des circuits quantiques de dimension supérieure
Emmanuel Jeandel, Simon Perdrix
A mathematical theory of legal texts' versioning
Luc Pellissier (LACL, Université Paris Est Créteil) & Samuel Mimram (LIX, École Polytechnique)
2.2 2.3.1
Implementation of cryptographic primitives on ML dedicated computational units
Jean-Pierre Flori - Apple Europe, Paris
Stochastic modeling of protein production within a growing cell population
Guillaume Ballif - Jakob Ruess - INRIA Saclay, Palaiseau
C2-19
Privacy on-demand and Security preserving Federated Generative Networks or Models
Frederic Giroire, Marco Lorenzi, Chuan Xu
Qualitative probabilistic hyperproperties and application to security
Benjamin Monmege and Jean-Marc Talbot. LIS, Aix-Marseille University
Learning Linear-time Temporal Logic
Adrien Pommellet, LRE, EPITA
2.16. Modèles de calcul et automates fini
Post-Quantum Statistical Zero-Knowledge Arguments for NP from Post-Quantum One-Way Functions
Quoc-Huy Vu, Céline Chevalier - ENS, Paris
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.
Various topics in cryptography and computer security
Michele Orrù
2.12.1-2, 2.34
The ecology of autocatalytic cycles, in the context of the origin of life
Sylvain Charlat