Sidebar
internships2020
Internships 2019/2020
- Dépliages de réseaux de Petri pour l'analyse d'écosystèmes
Franck Pommereau, université d'Évry/Paris-Saclay
- An integrated model for the cell
C. Gaucherel (and S. Haar) - Montpellier
Petri nets, network and symbolic dynamics - A qualitative model for evolution of ecosystems
C. Gaucherel (and M. Maximova) - Montpellier
Graph Transformations (Krivine) - Implementing a differential programming framework based on linear logic negation
Michele Pagani (and Alois Brunel, Damiano Mazza) - Paris
2.1, 2.2 - Bayesian networks and linear logic quantitative semantics
Michele Pagani (and Marco Gaboardi) - IRIF, Paris
2.1, 2.2 - Une sémantique formelle pour la fusion de changements de code source
Yann Régis-Gianas (IRIF) / David Mentré (MERCE)
- Une formalisation mécanisée du "Test driven development"
Yann Régis-Gianas (IRIF) / David Mentré (MERCE)
- Secure and efficient elliptic-curve signatures for emerging applications
Matthieu Rivain (CryptoExperts) - Paris
- Formalisation d’un langage graphique à bloc pour la preuve de programme
Dowek (LSV) - Belmonte (Alstom)
2.7.1, 2.7.2, 2.36.1 - 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 - Cryptanalyse quantique d'algorithmes symétriques
Zoé Amblard, Aurélien Dupin, Ange Martinelli (Thales)
- Schémas de chiffrement complétement homomorphe hybride pour une délégation de calculs efficace
Olivier Bernard, Thomas Ricosset (Thales)
- Implémentation optimisée de schémas de signature post-quantiques
Sylvain Lachartre, Thomas Ricosset (Thales)
- A domain specific language for formally verified legislation
Denis Merigoux, Karthikeyan Bhargavan : Inria (PROSECCO), Paris
- 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 - 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 - Enumération efficace des sommets d’un polyèdre en Coq
Xavier Allamigeon (CMAP), Pierre-Yves Strub (LIX) - École Polytechnique
2.7.1 - Quantum search as a naturally occurring phenomenon
Giuseppe Di Molfetta, Pablo Arrighi - LIS, Marseille
2.34.1 - Développement d'un greffon Frama-C pour la génération automatique d'annotations ACSL
Patricia MOUY ANSSI (Paris)
- Taming the Computational Complexity of Resource-Bounded Logics
Stéphane Demri – LSV, ENS Paris-Saclay
1.39, 1.22, 2.20.1 - Isometry-invariant tilings
Benjamin Hellouin de Menibus - LRI, Université Paris-Sud
Dynamique symbolique ; algorithmique des graphes ; - Nonabelian cellular automata
Benjamin Hellouin de Menibus - LRI, Université Paris-Sud
Dynamique symbolique - DNA computing: theory, models and wet lab experiments
Nicolas Schabanel - LIP, ENS de Lyon
2.11.1, 2.19 - Complex Analysis and Cauchy's Integral Theorem in Lean
Robert Y. Lewis, Jasmin Blanchette: Vrije Universiteit Amsterdam
- Algorithmic Fairness Static Analysis for Neural Networks
Caterina Urban - INRIA & École Normale Supérieure, Paris
2.6 - A General Framework for Input Data Uage Static Analysis
Caterina Urban - INRIA & École Normale Supérieure
2.6 - Generic and incremental model-based safety assessment
Rémi Delmas, Youssef Hamadi - Uber ATCP (Paris)
Programmation Fonctionnelle, Compilation, Verification formelle (SAT, SMT) - 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 - Calcul formel, systèmes polynomiaux et applications
Mohab Safey El Din, LIP6, Sorbonne Univ.
2-13-1 et 2-22 - 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 - 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 - Analyse des générateurs de parsers binaires pour le traitement des paquets réseau
Olivier Levillain (Télécom SudParis Evry ou Palaiseau)
- Learning to Rank Trees in a Heterogeneous Graph with Applications in Investigative Journalism
Oana Balalau, Ioana Manolescu, and Fabian Suchanek, location Inria Saclay
- Constraint-based disambiguation of label and field names in OCaml
Gabriel Scherer - INRIA Saclay
2.4 Functional programming and type systems - Low Level OCaml -- LowCaml
Gabriel Scherer - INRIA Saclay
2.4 Functional programming and type systems - 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
- Stage en Apprentissage statistique: Dialogue entre systèmes de recommandation
Olivier Cailloux, MCF, LAMSADE; Florian Yger, MCF, LAMSADE, Université Paris-Dauphine.
- 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 - Provenance for Ontology-Mediated Query Answering
Antoine Amarilli (Télécom Paris), Pierre Bourhis (Inria Lille)
Web Data Management 2.26.2 - Enumerating Query Results on Multitrees
Antoine Amarilli, Louis Jachiet, Luc Segoufin ; ENS Paris
2.26.1, 2.26.2 - ECDSA Attack with partial knowledge for the Nonce
Thomas Roche / Laurent Imbert - LIRMM (Montpellier, France)
Techniques en cryptographie et cryptoanalyse - Automated Transcription of Jazz Soli
Florent Jacquemard, Philippe Rigaux, Vertigo team, Cedric, CNAM Paris
1.18, 2.16, 2.27.1 - From Research Articles to a Structured Knowledge Base of Theorems
Pierre Senellart, ENS Paris
2-26-2 - Nouvelles fonctionnalités pour un compilateur Lustre formellement vérifié avec Coq
Timothy Bourke & Marc Pouzet - Inria/ENS
2-23-1 - Vérification déductive de programmes respectant une discipline de typage à la Rust
Jacques-Henri Jourdan - Univ. Paris-Saclay
2-36-1 - 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
- Specification and Verificationof Properties of Neural Networks
Serge Haddad - LSV
2.6, 2.8.2, 2.24.1 - Abstract Domain Reduction Operation Beween Separation Logic Memory Abstraction And Value Abstraction
Xavier Rival - ENS Paris/INRIA
2.6 - 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 - Cryptographie Post-Quantique et Environnements Contraints
Carlos Aguilar Melchor - ISAE SUPAERO (Toulouse)
Cryptographie - 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é
- 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 ;
internships2020.txt · Last modified: 2020/09/14 16:37 by carton