Internships 2019/2020

  1. Dépliages de réseaux de Petri pour l'analyse d'écosystèmes
    Franck Pommereau, université d'Évry/Paris-Saclay
  2. An integrated model for the cell
    C. Gaucherel (and S. Haar) - Montpellier
    Petri nets, network and symbolic dynamics
  3. A qualitative model for evolution of ecosystems
    C. Gaucherel (and M. Maximova) - Montpellier
    Graph Transformations (Krivine)
  4. Online Algorithms for Fair Ad Auctions
    Patrick Loiseau and Nicolas Gast, Inria/LIG (Grenoble)
  5. Implementing a differential programming framework based on linear logic negation
    Michele Pagani (and Alois Brunel, Damiano Mazza) - Paris
    2.1, 2.2
  6. Bayesian networks and linear logic quantitative semantics
    Michele Pagani (and Marco Gaboardi) - IRIF, Paris
    2.1, 2.2
  7. Une sémantique formelle pour la fusion de changements de code source
    Yann Régis-Gianas (IRIF) / David Mentré (MERCE)
  8. Une formalisation mécanisée du "Test driven development"
    Yann Régis-Gianas (IRIF) / David Mentré (MERCE)
  9. Développement d'une bibliothèque POSIX pour Coq
    Thomas Letan, ANSSI (Paris)
  10. A priori anatomiques et modèles multi-compartiments de diffusion pour la tractographie de la matière blanche cérébrale
    Olivier Commowick
  11. Secure and efficient elliptic-curve signatures for emerging applications
    Matthieu Rivain (CryptoExperts) - Paris
  12. Formalisation d’un langage graphique à bloc pour la preuve de programme
    Dowek (LSV) - Belmonte (Alstom)
    2.7.1, 2.7.2, 2.36.1
  13. Automatic Theorem Proving in Coq
    Valentin Blot, Gilles Dowek et Chantal Keller - Université Paris-Saclay
    Assistants de preuves, Fondements des systèmes de preuves, Démonstration automatique
  14. Developpement d'implementation threshold sur un banc DPA
    Renaud Dubois, Valentin Mascre (Thales)
  15. Cryptanalyse quantique d'algorithmes symétriques
    Zoé Amblard, Aurélien Dupin, Ange Martinelli (Thales)
  16. Schémas de chiffrement complétement homomorphe hybride pour une délégation de calculs efficace
    Olivier Bernard, Thomas Ricosset (Thales)
  17. Implémentation optimisée de schémas de signature post-quantiques
    Sylvain Lachartre, Thomas Ricosset (Thales)
  18. Sécurité des communications réseau de l’IoT
    Arnaud Ebalard, ANSSI (Paris)
  19. A domain specific language for formally verified legislation
    Denis Merigoux, Karthikeyan Bhargavan : Inria (PROSECCO), Paris
  20. Optimalité et analyse en moyenne de l'algorithme Git bisect
    Julien Courtiel, Paul Dorbec - GREYC, Caen
    Algorithmique des graphes / Aspects algorithmiques de la combinatoire / Calcul formel / Analyse d'algorithmes / Algorithmique et combinatoire des graphes géométriques
  21. Formal Methods for Security: automated low-level software security analysis
    Sébastien Bardin (CEA) – location: CEA Saclay
    all modules concerned with formal verification, especially: 2.5.1, 2.6, 2.9.2,2.36.1
  22. Study of possible instances of broadcast encryption
    Sébastien Canard - Orange Labs Caen
    cryptology
  23. Enumération efficace des sommets d’un polyèdre en Coq
    Xavier Allamigeon (CMAP), Pierre-Yves Strub (LIX) - École Polytechnique
    2.7.1
  24. Développement d’un outil d’analyse automatique d’applications Android
    Aurélien Deharbe (ANSSI)
  25. Efficient model-checking for the Electrum language
    David CHEMOUIL & Julien BRUNEL - ONERA Toulouse
  26. Grading LL-exponentials
    Flavien Breuvart and Damianon Mazza (LIPN)
    2.1, 2.2, 2.4
  27. Factorizing probabilistic intersection types
    Flavien Breuvart and Damianon Mazza (LIPN)
    2.1, 2.2,
  28. Quantum search as a naturally occurring phenomenon
    Giuseppe Di Molfetta, Pablo Arrighi - LIS, Marseille
    2.34.1
  29. Développement d'un greffon Frama-C pour la génération automatique d'annotations ACSL
    Patricia MOUY ANSSI (Paris)
  30. Taming the Computational Complexity of Resource-Bounded Logics
    Stéphane Demri – LSV, ENS Paris-Saclay
    1.39, 1.22, 2.20.1
  31. Isometry-invariant tilings
    Benjamin Hellouin de Menibus - LRI, Université Paris-Sud
    Dynamique symbolique ; algorithmique des graphes ;
  32. Nonabelian cellular automata
    Benjamin Hellouin de Menibus - LRI, Université Paris-Sud
    Dynamique symbolique
  33. DNA computing: theory, models and wet lab experiments
    Nicolas Schabanel - LIP, ENS de Lyon
    2.11.1, 2.19
  34. Complex Analysis and Cauchy's Integral Theorem in Lean
    Robert Y. Lewis, Jasmin Blanchette: Vrije Universiteit Amsterdam
  35. Variational methods for graph signal processing
    S. Vaiter - Dijon
  36. Algorithmic Fairness Static Analysis for Neural Networks
    Caterina Urban - INRIA & École Normale Supérieure, Paris
    2.6
  37. A General Framework for Input Data Uage Static Analysis
    Caterina Urban - INRIA & École Normale Supérieure
    2.6
  38. Generic and incremental model-based safety assessment
    Rémi Delmas, Youssef Hamadi - Uber ATCP (Paris)
    Programmation Fonctionnelle, Compilation, Verification formelle (SAT, SMT)
  39. Reinforcement Learning and Extreme Value Theory for Cyber Physical Systems Analysis
    Rémi Delmas, Eric Goubault - Uber ATCP (Paris)
    Systèmes Hybrides, Langages synchrones, Apprentissage par renforcement, optimisation stochastique, statistiques/probabilités,, Verification formelle, logiques temporelles
  40. A user interface for formal proofs
    Benjamin Werner, Pierre-Yves Strub
    2-7-1 2-7-2
  41. A user interface for formal proofs
    Benjamin Werner, Pierre-Yves Strub
    2-7-1 2-7-2
  42. Calcul formel, systèmes polynomiaux et applications
    Mohab Safey El Din, LIP6, Sorbonne Univ.
    2-13-1 et 2-22
  43. Sharing and Unsharing in Hindley Milner
    Didier Rémy
  44. Résolution numérique d'équations différentielles à singularités apparentes / Numerical Solution of ODEs with Apparent Singularities
    Marc Mezzarobba _marc.mezzarobba@lip6.fr_, LIP6 (Jussieu), Paris
    C-2-22
  45. Synthèse de code pour l'évaluation de fonctions de Bessel / Code Generation for the Evaluation of Bessel Functions
    Marc Mezzarobba _marc.mezzarobba@lip6.fr_, LIP6 (Jussieu), Paris
    C-2-22
  46. Propagation of type annotations inHindler-Milner based type-systems
    Didier Rémy
  47. Analyse des générateurs de parsers binaires pour le traitement des paquets réseau
    Olivier Levillain (Télécom SudParis Evry ou Palaiseau)
  48. Learning to Rank Trees in a Heterogeneous Graph with Applications in Investigative Journalism
    Oana Balalau, Ioana Manolescu, and Fabian Suchanek, location Inria Saclay
  49. Updates in Description Logics
    Stéphane Demri, ENS Paris-Saclay
    1.39, 1.22
  50. Characterization of NP or PSPACE with polynomial Ordinary Differential Equations. Continuous time Analog machines and models of computation
    Olivier Bournez
  51. Complexity theory with Discrete Differential Equations/Finite differences
    Olivier BOURNEZ
  52. Continuous Time Models of Computations and Computations Over the Ordinals
    Olivier Bournez
  53. Turing Neural Computer, Differential Neural Computer, Neural Stack Machine, Neural Network Pushdown Automata etc
    Olivier BOURNEZ
  54. Constraint-based disambiguation of label and field names in OCaml
    Gabriel Scherer - INRIA Saclay
    2.4 Functional programming and type systems
  55. Low Level OCaml -- LowCaml
    Gabriel Scherer - INRIA Saclay
    2.4 Functional programming and type systems
  56. Graph polynomials and symmetric functions
    J.-C. Aval, P. McNamara, A. Tanasa - LABRI
    Combinatorics
  57. Exploration expérimentale du jugement délibéré sur la décision d’établir une cantine scolaire végane
    Olivier Cailloux, Yves Meinard, Nicolas Salliou
  58. Stage en Apprentissage statistique: Dialogue entre systèmes de recommandation
    Olivier Cailloux, MCF, LAMSADE; Florian Yger, MCF, LAMSADE, Université Paris-Dauphine.
  59. MLF type inference and semi-unification
    Didier Rémy
    2.4
  60. Version discrète du partage du gâteau
    Frédéric Meunier - École des Ponts
  61. Verification of Chunk Sequences
    Arthur Charguéraud, Inria, Strasbourg et François Pottier, Inria, Paris
    2.4,2.36.1,2.7.1,2.7.2
  62. Streaming Algorithms for Submodular Function Optimisation
    Chien-Chung Huang
  63. Coarse Graining of Quantum Cellular Automata
    Di Molfetta - Marseille
  64. Quantum Walking over a discrete sphere
    Di Molfetta - LIS, Marseille
  65. Manhattan Inhomogeneous Walk over directed graphs
    Di Molfetta - LIS, Marseille
  66. Searching in non-linear computing
    Di Molfetta - LIS, Marseille
  67. Provenance for Ontology-Mediated Query Answering
    Antoine Amarilli (Télécom Paris), Pierre Bourhis (Inria Lille)
    Web Data Management 2.26.2
  68. Enumerating Query Results on Multitrees
    Antoine Amarilli, Louis Jachiet, Luc Segoufin ; ENS Paris
    2.26.1, 2.26.2
  69. Algorithms for Finding Quasi Cliques in Large Graphs
    Mauro Sozio - Telecom Paris - Palaiseau
  70. Dynamic Trajectory Clustering
    Mauro Sozio - Telecom Paris - Palaiseau
  71. Dynamic Approximation Algorithms for Clustering
    Mauro Sozio - Telecom Paris - Palaiseau
  72. Familial monads and structural operational semantics
    Tom Hirschowitz - Chambéry
    2.2,2.3.1,2.4
  73. Recherche de fonctions par types
    Gabriel Radanne (Cambium)
  74. ECDSA Attack with partial knowledge for the Nonce
    Thomas Roche / Laurent Imbert - LIRMM (Montpellier, France)
    Techniques en cryptographie et cryptoanalyse
  75. Automated Transcription of Jazz Soli
    Florent Jacquemard, Philippe Rigaux, Vertigo team, Cedric, CNAM Paris
    1.18, 2.16, 2.27.1
  76. From Research Articles to a Structured Knowledge Base of Theorems
    Pierre Senellart, ENS Paris
    2-26-2
  77. Online Computation with Untrusted Advice
    Spyros Angelopoulos, LIP6, Sorbonne University
  78. Online Searching with Earliest Clearance
    Spyros Angelopoulos, LIP6, Sorbonne University
  79. Nouvelles fonctionnalités pour un compilateur Lustre formellement vérifié avec Coq
    Timothy Bourke & Marc Pouzet - Inria/ENS
    2-23-1
  80. Vérification déductive de programmes respectant une discipline de typage à la Rust
    Jacques-Henri Jourdan - Univ. Paris-Saclay
    2-36-1
  81. Garanties d’exécution de programmes OCaLustre et OCaml pour microcontrôleurs
    Emmanuel Chailloux - Steven Varoumas (équipe APR - LIP6 - Sorbonne Université - campus Jussieu - Paris)- steven.varoumas@lip6.fr
  82. WhiteBox Cryptography
    Thomas Icart - Paris 16
  83. Specification and Verificationof Properties of Neural Networks
    Serge Haddad - LSV
    2.6, 2.8.2, 2.24.1
  84. Sampling Landscape Features
    Benjamin Doerr, Carola Doerr, Johann Dreo - LIX (Ecole Polytechnique)
  85. Abstract Domain Reduction Operation Beween Separation Logic Memory Abstraction And Value Abstraction
    Xavier Rival - ENS Paris/INRIA
    2.6
  86. Concurrent Data Structures for Big Data Streaming
    Petr Kuznetsov (Telecom Paris), Albert Biffet Telecom Paris), Panagiota Fatourou (U Crete)
    2.18.2, 2.29.2
  87. Local Reasoning about Reconfigurable Component-based Systems
    Radu Iosif - Verimag
  88. Verifying Concurrent Systems with Automata over Infinite Alphabets
    Radu Iosif - Verimag
  89. Cryptocurrencies in Systems with Decentralized Trust
    Petr Kuznetsov (Telecom Paris)
    2.18.2, 2.18.1
  90. Cryptographie Post-Quantique et Environnements Contraints
    Carlos Aguilar Melchor - ISAE SUPAERO (Toulouse)
    Cryptographie
  91. Résolubilité dans le modèle Heard-Of
    B. Charron-Bost- LIX
  92. Encodage et résolution de jeux à 2 joueurs pour des réseaux de robots collaboratifs, par une approche basée sur les SAT-solvers
    Souheib Baarir, Nathalie Sznajder, Sébastien Tixeuil - LIP6, Sorbonne Université
  93. Liens entre groupes et pavages
    Pascal Vanier - LACL
  94. Formal Methods, Safety and AI
    Zakaria Chihani - CEA Paris Saclay
    2.36.1 Proofs of programs ; 2.35.1 Constraint programming ; 2.9.2 Algorithmic verification of programs 2.7.2 Proof assistants ; 2.7.1 Foundations of proof systems ; 2.5.1 Automated deduction ; 2.6 Abstract interpretation: application to verification and static analysis ;2-4 Functional programming and type systems ; 1-36 Initiation to research ; 1-39 Logical aspects of artificial intelligence ;1-22 Basics of verification ; 1-35 Introduction to Computer Vision ;