===== Internships 2014/2015 =====
- Les représentations équivalentes d'un LFSR filtré et leur impact en cryptanalyse
Anne Canteaut - Inria Rocquencourt
2.13.2 et 2.12.1 - Behaviours as solutions for higher-order programs and processes
Daniel Hirschkoff, ENS Lyon
2.3 (2.2) - A dynamical system approach to compute the transient behavior of stochastic distributed systems.
Nicolas Gast, Bruno Gaujal. Inria Grenoble
2.17.1 (network modeling) and 2.18.1 (Distributed Algorithms for Networks) - Vehicle Sharing Systems: Analysis, modeling, simulation, optimization
Nicolas GAST - INRIA Monbonnot and Vincent JOST - CNRS G-SCOP Grenoble
- Evaluation efficace de polynômes sur les corps finis et application aux implémentations sécurisées contre les attaques par canaux auxiliaires
Matthieu Rivain, CryptoExperts, Paris
Cryptography - Types and interpretations for programs of polynomial time complexity
Patrick Baillot, ENS Lyon
2.2, 2.1 (2.4) - Résolution symbolique efficace de systèmes d’équations linéaires différentielles et de récurrences
Frédéric Chyzak et Alin Bostan
- Calcul efficace de coefficients de séries
Frédéric Chyzak et Alin Bostan - INRIA Saclay ÎDF (à Palaiseau)
- Preuves algorithmiques pour la transcendance des séries
Frédéric Chyzak et Alin Bostan - INRIA Saclay ÎDF (à Palaiseau)
- FouCo : support pour les définitions corécursives dans l'assistant de preuves Isabelle/HOL
Jasmin Blanchette - Inria Nancy ou Max-Planck-Institut für Informatik à Sarrebruck (Allemagne)
1-20, 1-22, 1-36, 2.5.1, 2.7.2, 2.36.1 - Relativized Implicit Computational Complexity and Declassification
Frédéric Prost - LIP ENS-Lyon
2.1 / 2.6 / - Translation methods for deciding separation logics
Stéphane Demri – LSV, ENS Cachan
2.5.1, 2.9.1, 2.9.2, 2.36.1 - www.prism.uvsq.fr/~ystr/stage.html
Laboratoire PRiSM, Université de Versaille Saint QUentin
Techniques de théorie des jeux en informatique - Verification of Distributed Systems with Parameterized Network Topology
Benedikt Bollig & Paul Gastin (LSV, ENS Cachan)
2-3; 2-8; 2-9; 2-16; 2-20 - Études des algorithmes pour différentes classes de jeux stochastiques, jeux représentés implicitement
Yann Strozecki, Université de Versailles Saint Quentin, PRiSM
Techniques de théorie des jeux en informatique - Complexité d'énumération : séparation de classes et bornes inférieures
Yann Strozecki, Université de Versailles Saint Quentin, PRiSM
2.26.1, 2.31.1, 2.33.1 - Modèles mécaniques formels pour l'algorithmique distribuée (essaims de robots)
Xavier Urbain, LRI (PCRI, Orsay)
2.7.2 - Modèles mécaniques formels pour l'algorithmique distribuée (comportements probabilistes)
Xavier Urbain, LRI (PCRI, Orsay)
2.7 - Graphes plongés sur les surfaces: algorithmes pour la génération et le plongement
Luca Castelli Aleardi (Ecole Polytechnique)
2-38-1 - Optimisation et réécriture de requêtes sous constraintes : Graphes , Arbres et mots
Sophie Tison et Pierre Bourhis - LIFL & INRIA LILLE
1-18; 2.16; 2.26.1; 2.26.2 - Distributed Algorithms Run By Selfish Agents
Pierre Fraigniaud and Paolo Penna, LIAFA, Univ. Paris Diderot
2.18.1 - Exploring the Limits of Distributed Computation: Local Graph Coloring
Pierre Fraigniaud and Adrian Kosowski, LIAFA, Univ. Paris Diderot
2.18.1 - Réseaux sociaux: outils géométriques et combinatoires pour l'analyse et visualisation des réseaux complexes
Luca Castelli Aleardi et Maks Ovsjanikov (Ecole Polytechnique)
2-38-1 - Plongements topologiques de graphes dans des 2-complexes simpliciaux
Éric Colin de Verdière - ENS Ulm (Paris 5ème)
2-38-1, 2-29-1, 2-14-1 - Décroisements de graphes dans le plan avec obstacles
Éric Colin de Verdière - ENS Ulm (Paris 5ème)
2-38-1, 2-29-1, 2-14-1 - Approche par contrats pour la sûreté de fonctionnement dans les systèmes critiques "cyber-physiques"
Daniela Cancila - CEA Saclay, Nanoinnov
2.3, 2.16, 2.23.1, 2.36.1, 2.37.1 - Verifying replicated data structures: causal consistency
Ahmed Bouajjani and Constantin Enea - LIAFA, Univ. Paris Diderot
2.3 - 2.9.2 - 2.18.2 - Verification of Haskell Programs
Matthew Hague, Royal Holloway University of London
1-22, 2.4, 2.6, 2.9.1, 2.9.2, 2.16 - Formalisation and certification of ownership in a specialised Java virtual machine
Damien Pous, LIP, ENS Lyon
- Evaluation et amélioration de la sécurité des implémentations de cryptographie symétrique
Julien Bringer - Morpho - Osny
2.12 2.13 2.30 - Type refinement in λΠ-calculus modulo
Arnaud Spiwack & Olivier Hermant – Deducteam, Inria Paris-Rocquencourt & CRI, MINES ParisTech
2.7.1, 2.7.2, 2.1, 2.4 - From Completeness to Normalization
Olivier Hermant (Mines and Inria Paris)
2.7.1 (Foundations of Proof Systems) and 2.7.2 (Proof Assistants) - QuickChick: Property-Based Testing for Coq
Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)
1-20, 1-22, 1-24, 1-31, 2.1, 2.4, 2.5.1, 2.6, 2.7.1, 2.7.2, 2.36.1 - Querying Probabilitistic Data via Tree Decompositions
Pierre Senellart - Télécom ParisTech & National University of Singapore
2.26.2, 2.26.1, 2.16 - Canonical form of Boolean network & properties
Franck Delaplace - IBISC LAB, Tarek Melliti - IBISC LAB
I32, - 3D Time-Traveler: Interpolation Interactive 3D+T
Julien Tierny _julien.tierny@lip6.fr_, Julie Delon _julie.delon@parisdescartes.fr_, Sorbonne Universites UPMC - LIP6, Paris (Metro 7,10)
- inSitu Topology: Visualisation pour le Calcul Haute Performance
Julien Tierny _julien.tierny@lip6.fr_, Sorbonne Universites UPMC - LIP6, Paris (Metro 7, 10)
- Construction de graphes de Reeb et squelettes topologiques pour la visualisation des champs scalaires dans le logiciel Open-Source ParaView
Alejandro Ribes _alejandro.ribes@edf.fr_, Julien Tierny _julien.tierny@lip6.fr_, EDF Clamart
- Sémantique formelle des proxies de la prochaine version de JavaScript
Alan Schmitt - Inria Rennes
2.7.2, 2.36.1 - Proof of convergence for a spacecraft guidance rendezvous algorithm
M. Joldes, C. Louembet - LAAS-CNRS, Toulouse
- Étude combinatoire d'arbres et d'arrangements d'hyperplans
Sylvie Corteel (LIAFA Universite Paris Diderot et David Forge (LRI, Universite Paris Sud)) corteel@liafa.univ-paris-diderot.fr, forge@lri.fr
C2-10 - Data intensive management systems concurrency control Coq mechanization
V. Benzaken, É. Contejean, LRI - CNRS Orsay
- Étude logique de l'ordonnancement dans les algèbres de processus
Emmanuel Beffara - LIP, ENS Lyon
1.20, 2.1, 2.2, 2.3, 2.4 - Define an internalization of Homotopy Type Theory in Coq
N. Tabareau/M. Sozeau - Inria, Nantes-Paris
2.7.2 - Define and implement a general notion of higher inductive types
N. Tabareau/M. Sozeau - Inria, Nantes-Paris
2.7.2 - Parallel algorithms for geometric information analysis from 3D scanners
Sylvain Contassot-Vivier and Adrien Krähenbühl - LORIA Nancy
- Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)
2.4, 2.5.1, 2.6, 2.7.2, 2.36.1 - Étude de la résistance des algorithmes de cryptographie légère face aux attaques physiques
Jacques Fournier - CEA LSAS, Centre Micro-électronique de Provence, Gardanne (13)
2.13.2 et 2.12.1 - Optimal mechanisms for the protection of confidential information
Catuscia Palamidessi and Konstantinos Chatzikokolakis. INRIA and Ecole Polytechnique
- A New Operational Semantics for the Focalized Intuitionistic Sequent Calculus
Delia Kesner - PPS - Univ. Paris-Diderot
- Analyse de la sécurité d'algorithmes de chiffrement authentifié
Thomas Fuhr et Henri Gilbert - ANSSI, Paris
- Verified JIT compilation of Coq
Xavier Leroy, Maxime Dénès – Inria Paris-Rocquencourt
2-4, 2-7-1, 2-7-2 - Vérification formelle d’analyses de complexité
Francois Pottier et Arthur Charguéraud, INRIA Paris-Rocquencourt
2.4, 2.7.2, 2.36.1 - A game-theoretic approach to controller synthesis for the acrobot swing-up problem
Nicolas Perrin - Paris
2.8.2, 2.20.1, 1-19, 1-22 - Conception et implémentation d’un outil et d’une librairie OCaml pour manipuler les lieurs
Francois Pottier, INRIA Paris-Rocquencourt
2.4 - Games of imperfect information over graphs
Patricia Bouyer (LSV), Samson Lasaulce (L2S), Nicolas Markey (LSV)
2.20.1, 1.22, 1.24 - Vérification de preuves d'arithmétique dans le lambda-Pi-calcul modulo
David Delahaye - Inria Paris (Place d'Italie)
2.5.1, 2.7.1, 2.7.2, 2.36.1 - Une approche inspirée de l'archéologie pour l'analyse de données de votes dans une élection
Olivier Spanjaard, Fanny Pascual - Sorbonne Universités Univ Paris 06, Laboratoire d'Informatique de Paris 6
Algorithmique, optimisation combinatoire, complexité - Static analysis by abstract interpretation of the functional correctness of vector and matrix manipulating programs
Antoine Miné - École normale supérieure
2.6 - Analyse des erreurs d'arrondi d'une bibliothèque d'analyse numérique
Sylvie Boldo - Inria Saclay
2.36.1 - Algorithmic issues in MapReduce
E. Bampis, G. Lucarelli, D. Trystram - INRIA Grenoble or LIP6
2.24.1, 2.29.1 - conception et la programmation d'algorithmes de reconstruction de codes correcteurs d'erreurs
Pierre Loidreau - Direction générale de l'armement (Rennes)
2.13.2 - Deciding rational functions among regular ones using streaming string transducers
Pierre-Alain Reynier (LIF)
2.16 - Approximation Algorithms for Combinatorial Optimization Problems in Geometry
Nabil Mustafa - LIGM Universite Paris-Est
- F*: SMT-Based Verification for ML
Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)
2.4, 2.7.2, 2.36.1, 2.5.1, 2.7.1, 2.6, 2.1 - Evolutionary Algorithm: Mixture-Model Extension of CMA-ES for Multi-Modal Optimization
François Fages - Inria Paris-Rocquencourt
2.24.1, 2.19 - Tropical constraint methods for reducing biochemical reaction systems with multiple timescales
François Fages - Inria Paris-Rocquencourt
2.19, 2.13.1 - Boucles de rétroaction positive et multistationarité dans des systèmes de réactions biochimiques
Sylvain Soliman - Inria Paris-Rocquencourt
C2.19, C2.29.1 - Inférence de modèle réactionnel correspondant à un graphe d’influence
François Fages et Sylvain SOliman - Inria Paris-Rocquencourt
C2.19, C2.6 - Approximation Algorithms for Combinatorial Optimization Problems in Geometry
Nabil Mustafa - LIGM Universite Paris-Est
- Proof Engineering Tools for Coq
Eelco Visser and Pierre Neron and Andrew Tolmach - TU Delft - Netherlands)
2.7.2 2.4 - Accurate and Efficient Disjunctions of Abstract Properties of Memory States
Xavier Rival - DIENS
2.6 - Formal Study of a Countermeasure Against Side-Channel Attacks
Pablo Rauzy and Sylvain Guilley, at Télécom ParisTech
- Protecting Elliptic Curve Cryptography Against Fault Injection Attacks
Pablo Rauzy and Sylvain Guilley, at Télécom ParisTech
- A weakly relational domain to detect potential polymerisation events in signaling pathways
J Feret, DI - Ecole normale supérieure, 75005 Paris
M2 - 6: Abstract interpretation - Approximate model reduction for the differential semantics of rule-based models
J Feret, DI - Ecole normale supérieure, 75005 Paris
M2 - 6: Abstract interpretation - Algorithmes de Partitionnement de Graphes Dynamiques - Dynamic Graphs Partitionning Algorithms
Nicolas Schabanel - LIAFA (U. Paris Diderot)
2.11.1, ,1.24, 2.11.2, 2.18.1, 2.24.1, 2.29.1, 2.38.1 - Gelfand duality for compact partially ordered spaces
Emmanuel Haucourt - École Polytechnique (LIX)
Concurrency 2.3 - Strong normalisation for simply typed lambda-calculus: a quest for new combinatorial proofs
Stefano Guerrini, Giulio Manzonetto
2.1, 2.2 et 2.4 - Résolution de contraintes pour la vérification de programmes
Sébastien Bardin, CEA LIST (Paris-Saclay)
- Génération automatique d'exploits à partir de traces d'erreurs
Marie-Laure Potet, Laurent Mounier (Verimag), Sébastien Bardin (CEA)
- Negotiation of correspondence policies
A.Bouabdallah - L.Cailleux / Location = DGA/MI (Bruz) or Telecom Bretagne (Rennes)
- Categorical Semantics of Distributed Version Control Systems
Samuel Mimram (LIX, École Polytechnique)
1-20, 2.2 - Categorical Semantics of Distributed Version Control Systems
Samuel Mimram (LIX, École Polytechnique)
1-20, 2.2 - Categorical Semantics of Distributed Version Control Systems
Samuel Mimram (LIX, École Polytechnique)
1-20, 2.2 - Validation of distributed protocols for opportunistic networks
Franck Petit, Swan Dubois, UPMC/Inria
2.18.1