Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

internships2015 [2015/05/21 12:23] (current)
amadio created
Line 1: Line 1:
 +      ===== Internships 2014/2015 =====
 +**[[internship_submit|Submit an internship offer]]**
 +  - **[[https://www.rocq.inria.fr/secret/Anne.Canteaut/MPRI/stage.pdf|Les représentations équivalentes d'un LFSR filtré et leur impact en cryptanalyse]]** \\ <color grey>Anne Canteaut - Inria Rocquencourt</color>\\ <color grey>2.13.2 et 2.12.1</color>
 +  - **[[http://www.avoine.net/irisa_emsec_avoine_1.pdf|Analysis of the Mifare Plus Distance Bounding Protocol]]** \\ <color grey>Gildas Avoine, IRISA Rennes</color>\\ <color grey></color>
 +  - **[[http://www.avoine.net/irisa_emsec_avoine_3.pdf|Can SSD Memory Improve Cryptanalytic Time-Memory Trade-O ff?]]** \\ <color grey>Gildas Avoine, IRISA Rennes</color>\\ <color grey></color>
 +  - **[[http://www.avoine.net/irisa_emsec_avoine_2.pdf|Practical Cryptanalysis of Pseudo-Random Number Generators in RFID]]** \\ <color grey>Gildas Avoine</color>\\ <color grey></color>
 +  - **[[http://perso.ens-lyon.fr/daniel.hirschkoff/Stages/dh-contr.pdf|Behaviours as solutions for higher-order programs and processes]]** \\ <color grey>Daniel Hirschkoff, ENS Lyon</color>\\ <color grey>2.3 (2.2)</color>
 +  - **[[http://mescal.imag.fr/membres/nicolas.gast/news/2014/10/10/intership-hittingTime/index.html|A dynamical system approach to compute the transient behavior of stochastic distributed systems.]]** \\ <color grey>Nicolas Gast, Bruno Gaujal. Inria Grenoble</color>\\ <color grey>2.17.1 (network modeling) and 2.18.1 (Distributed Algorithms for Networks)</color>
 +  - **[[http://mescal.imag.fr/membres/nicolas.gast/news/2014/10/10/intership-BSS/index.html|Vehicle Sharing Systems: Analysis, modeling, simulation, optimization]]** \\ <color grey>Nicolas GAST - INRIA Monbonnot and Vincent JOST - CNRS G-SCOP Grenoble</color>\\ <color grey></color>
 +  - **[[http://www.cryptoexperts.com/cryptoexperts_offre_stage.pdf|Evaluation efficace de polynômes sur les corps finis et application aux implémentations sécurisées contre les attaques par canaux auxiliaires]]** \\ <color grey>Matthieu Rivain, CryptoExperts, Paris</color>\\ <color grey>Cryptography</color>
 +  - **[[http://perso.ens-lyon.fr/patrick.baillot/STAGES/2015/sujet_interpretations2015.pdf|Types and interpretations for programs of polynomial time complexity]]** \\ <color grey>Patrick Baillot, ENS Lyon</color>\\ <color grey>2.2, 2.1 (2.4)</color>
 +  - **[[http://specfun.inria.fr/internships/|Résolution symbolique efficace de systèmes d’équations linéaires différentielles et de récurrences]]** \\ <color grey>Frédéric Chyzak et Alin Bostan</color>\\ <color grey></color>
 +  - **[[http://specfun.inria.fr/internships/|Calcul efficace de coefficients de séries]]** \\ <color grey>Frédéric Chyzak et Alin Bostan - INRIA Saclay ÎDF (à Palaiseau)</color>\\ <color grey></color>
 +  - **[[http://specfun.inria.fr/internships/|Preuves algorithmiques pour la transcendance des séries]]** \\ <color grey>Frédéric Chyzak et Alin Bostan - INRIA Saclay ÎDF (à Palaiseau)</color>\\ <color grey></color>
 +  - **[[http://www21.in.tum.de/~blanchet/corec.pdf|FouCo : support pour les définitions corécursives dans l'assistant de preuves Isabelle/HOL]]** \\ <color grey>Jasmin Blanchette - Inria Nancy ou Max-Planck-Institut für Informatik à Sarrebruck (Allemagne)</color>\\ <color grey>1-20, 1-22, 1-36, 2.5.1, 2.7.2, 2.36.1</color>
 +  - **[[http://perso.ens-lyon.fr/frederic.prost/Oracles.htm|Relativized Implicit Computational Complexity and Declassification]]** \\ <color grey>Frédéric Prost - LIP ENS-Lyon</color>\\ <color grey>2.1 / 2.6 / </color>
 +  - **[[http://www.lsv.ens-cachan.fr/~demri/m2-14-sd.pdf|Translation methods for deciding separation logics]]** \\ <color grey>Stéphane Demri -- LSV, ENS Cachan</color>\\ <color grey>2.5.1, 2.9.1, 2.9.2, 2.36.1</color>
 +  - **[[www.prism.uvsq.fr/~ystr/stage.html|]]** \\ <color grey>Laboratoire PRiSM, Université de Versaille Saint QUentin</color>\\ <color grey> Techniques de théorie des jeux en informatique </color>
 +  - **[[http://www.lsv.ens-cachan.fr/~bollig/MPRI/stage-M2.pdf|Verification of Distributed Systems with Parameterized Network Topology]]** \\ <color grey>Benedikt Bollig & Paul Gastin (LSV, ENS Cachan)</color>\\ <color grey>2-3; 2-8; 2-9; 2-16; 2-20</color>
 +  - **[[http://www.prism.uvsq.fr/~ystr/stages.html|Études des algorithmes pour différentes classes de jeux stochastiques, jeux représentés implicitement]]** \\ <color grey>Yann Strozecki, Université de Versailles Saint Quentin, PRiSM</color>\\ <color grey>Techniques de théorie des jeux en informatique </color>
 +  - **[[http://www.prism.uvsq.fr/~ystr/stages.html|Complexité d'énumération : séparation de classes et bornes inférieures]]** \\ <color grey>Yann Strozecki, Université de Versailles Saint Quentin, PRiSM</color>\\ <color grey>2.26.1, 2.31.1, 2.33.1</color>
 +  - **[[http://pactole.lri.fr/pub/M2_1415.pdf|Modèles mécaniques formels pour l'algorithmique distribuée (essaims de robots)]]** \\ <color grey>Xavier Urbain, LRI (PCRI, Orsay)</color>\\ <color grey>2.7.2</color>
 +  - **[[http://pactole.lri.fr/pub/M2_1415_prob.pdf|Modèles mécaniques formels pour l'algorithmique distribuée (comportements probabilistes)]]** \\ <color grey>Xavier Urbain, LRI (PCRI, Orsay)</color>\\ <color grey>2.7</color>
 +  - **[[http://perso.telecom-paristech.fr/~kuznetso/projects/SDN/cpc.pdf|Synchronization and Concurrency in Software-Defined Networking ]]** \\ <color grey>Petr Kuznetsov, ENST</color>\\ <color grey>2.3</color>
 +  - **[[http://perso.telecom-paristech.fr/~kuznetso/projects/Concur/concur.pdf|Highly Concurrent Data Structures ]]** \\ <color grey>Petr Kuznetsov, ENST</color>\\ <color grey>2.3</color>
 +  - **[[http://perso.telecom-paristech.fr/~kuznetso/projects/AT/at.pdf|Mathematics for Efficient and Robust Distributed Computing]]** \\ <color grey>Petr Kuznetsov, ENST</color>\\ <color grey>2.3</color>
 +  - **[[http://www.lix.polytechnique.fr/~pilaud/stages/stage_MPRI14_DPRibons.pdf|Arrangements of DP-ribbons]]** \\ <color grey>Michel Pocchiola (Paris 6) & Vincent Pilaud (École Polytechnique)</color>\\ <color grey>2-38-1</color>
 +  - **[[http://www.lix.polytechnique.fr/~pilaud/stages/stage_MPRI14_multitriangulationsSurfaces.pdf|Multitriangulations de surfaces]]** \\ <color grey>Vincent Pilaud (École Polytechnique)</color>\\ <color grey>2-38-1</color>
 +  - **[[http://www.lix.polytechnique.fr/~amturing/stages.html|Graphes plongés sur les surfaces: algorithmes pour la génération et le plongement]]** \\ <color grey>Luca Castelli Aleardi (Ecole Polytechnique)</color>\\ <color grey>2-38-1</color>
 +  - **[[http://www.lifl.fr/~bourhis/m2.pdf|Optimisation et réécriture de requêtes sous constraintes : Graphes , Arbres et mots]]** \\ <color grey>Sophie Tison et Pierre Bourhis - LIFL & INRIA LILLE</color>\\ <color grey>1-18; 2.16; 2.26.1; 2.26.2</color>
 +  - **[[http://www.liafa.univ-paris-diderot.fr/~pierref/MPRI/intership-GT.pdf|Distributed Algorithms Run By Selfish Agents]]** \\ <color grey>Pierre Fraigniaud and Paolo Penna, LIAFA, Univ. Paris Diderot</color>\\ <color grey>2.18.1</color>
 +  - **[[http://www.liafa.univ-paris-diderot.fr/~pierref/MPRI/internship-coloring.pdf|Exploring the Limits of Distributed Computation: Local Graph Coloring]]** \\ <color grey>Pierre Fraigniaud and Adrian Kosowski, LIAFA, Univ. Paris Diderot</color>\\ <color grey>2.18.1</color>
 +  - **[[http://sites.onera.fr/stages/sites/sites.onera.fr.stages/files/DTIM-2015-18.pdf|Decision procedures for FOLTL]]** \\ <color grey>Julien Brunel - ONERA - Toulouse</color>\\ <color grey></color>
 +  - **[[http://sites.onera.fr/stages/sites/sites.onera.fr.stages/files/DTIM-2015-22_0.pdf|Temporal multi-agent logic for requirement modelling]]** \\ <color grey>Julien Brunel - ONERA - Toulouse</color>\\ <color grey></color>
 +  - **[[http://www.lix.polytechnique.fr/~amturing/stages.html|Réseaux sociaux: outils géométriques et combinatoires pour l'analyse et visualisation des réseaux complexes]]** \\ <color grey>Luca Castelli Aleardi et Maks Ovsjanikov (Ecole Polytechnique)</color>\\ <color grey>2-38-1</color>
 +  - **[[http://www.di.ens.fr/~colin/cours/14mpri/embed-simpl-compl.pdf|Plongements topologiques de graphes dans des 2-complexes simpliciaux]]** \\ <color grey>Éric Colin de Verdière - ENS Ulm (Paris 5ème)</color>\\ <color grey>2-38-1, 2-29-1, 2-14-1</color>
 +  - **[[http://www.di.ens.fr/~colin/cours/14mpri/untangle-graphs.pdf|Décroisements de graphes dans le plan avec obstacles]]** \\ <color grey>Éric Colin de Verdière - ENS Ulm (Paris 5ème)</color>\\ <color grey>2-38-1, 2-29-1, 2-14-1</color>
 +  - **[[http://www.drt-cea.com/index.php/default/offresstage/default/?theme=Electronique%20-%20Electricit%E9&domaine=Electronique%20embarqu%E9e|Approche par contrats pour la sûreté de fonctionnement dans les systèmes critiques "cyber-physiques"]]** \\ <color grey>Daniela Cancila - CEA Saclay, Nanoinnov</color>\\ <color grey>2.3, 2.16, 2.23.1, 2.36.1, 2.37.1</color>
 +  - **[[http://www.liafa.univ-paris-diderot.fr/~cenea/RDS_internship.pdf|Verifying replicated data structures: causal consistency]]** \\ <color grey>Ahmed Bouajjani and Constantin Enea - LIAFA, Univ. Paris Diderot</color>\\ <color grey>2.3 - 2.9.2 - 2.18.2</color>
 +  - **[[http://www.cs.rhul.ac.uk/home/hague/files/masters-ad.html|Verification of Haskell Programs]]** \\ <color grey>Matthew Hague, Royal Holloway University of London</color>\\ <color grey>1-22, 2.4, 2.6, 2.9.1, 2.9.2, 2.16</color>
 +  - **[[https://team.inria.fr/regal/job-offers/masters-internship-a-distributed-log-for-scalable-big-data-storage/| A distributed log for scalable big-data storage]]** \\ <color grey>Alejandro Tomsic, IP6 (Paris)</color>\\ <color grey></color>
 +  - **[[https://team.inria.fr/regal/job-offers/masters-internship-version-management-for-big-data-storage/|Version management for big-data storage]]** \\ <color grey>Marc Shapiro, LIP6 (Paris)</color>\\ <color grey></color>
 +  - **[[http://perso.ens-lyon.fr/damien.pous/stages.html|Coinductive and symbolic algorithms for non standard automata]]** \\ <color grey>Damien Pous, LIP, ENS Lyon</color>\\ <color grey></color>
 +  - **[[http://perso.ens-lyon.fr/damien.pous/stages.html|Formalisation and certification of ownership in a specialised Java virtual machine]]** \\ <color grey>Damien Pous, LIP, ENS Lyon</color>\\ <color grey></color>
 +  - **[[http://perso.ens-lyon.fr/damien.pous/stages.html|PiCoq: pi-calculus within Coq]]** \\ <color grey>Damien Pous, LIP, ENS Lyon</color>\\ <color grey></color>
 +  - **[[http://crypt-rl.net/stages/MPH-masquage-stage2014-15.pdf|Evaluation et amélioration de la sécurité des implémentations de cryptographie symétrique]]** \\ <color grey>Julien Bringer - Morpho - Osny</color>\\ <color grey>2.12 2.13 2.30</color>
 +  - **[[http://crypt-rl.net/stages/MPH-smc-stage2014-15.pdf|Calcul sécurisé efficace et sûr]]** \\ <color grey>Julien Bringer - Morpho - Issy-Les-Moulineaux</color>\\ <color grey>2.12 2.13 2.30</color>
 +  - **[[http://crypt-rl.net/stages/MPH-vc-stage2014-15.pdf|Calcul vérifiable pour la biométrie]]** \\ <color grey>Julien Bringer - Morpho - Issy-Les-Moulineaux</color>\\ <color grey>2.12 2.13 2.30</color>
 +  - **[[http://assert-false.net/arnaud/internships/deduktife.pdf|Type refinement in λΠ-calculus modulo]]** \\ <color grey>Arnaud Spiwack & Olivier Hermant -- Deducteam, Inria Paris-Rocquencourt & CRI, MINES ParisTech</color>\\ <color grey>2.7.1, 2.7.2, 2.1, 2.4</color>
 +  - **[[https://www.irisa.fr/visages/_media/positions/inria_stage_qtshanoir_2015.pdf|QtShanoir, un service web pour l’interopérabilité entre systèmes de gestion et de traitement des données en imagerie médicale]]** \\ <color grey>Justine Guillaumont - Rennes</color>\\ <color grey></color>
 +  - **[[http://cri.ensmp.fr/people/hermant/docs/2015/nbc.pdf|From Completeness to Normalization]]** \\ <color grey>Olivier Hermant (Mines and Inria Paris)</color>\\ <color grey>2.7.1 (Foundations of Proof Systems) and 2.7.2 (Proof Assistants)</color>
 +  - **[[http://lacl.univ-paris12.fr/gava/stages/ProofCompilePetriNets.pdf|Compilation certifiée de réseaux de Petri colorés]]** \\ <color grey>Frédéric Gava (LACL) et Franck Pommereau (IBISC)</color>\\ <color grey></color>
 +  - **[[http://lacl.univ-paris12.fr/gava/stages/ABCDtoMPI.pdf|Implantation distribué de modèles concurrents]]** \\ <color grey>Frédéric Gava (LACL) et Franck Pommereau (IBISC)</color>\\ <color grey></color>
 +  - **[[http://lacl.univ-paris12.fr/gava/stages/ProofModelChecking.pdf|Vérification d'algorithmes de Model checking]]** \\ <color grey>Frédéric Gava et Julien Tesson (LACL)</color>\\ <color grey></color>
 +  - **[[http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2015/quick-chick.pdf|QuickChick: Property-Based Testing for Coq]]** \\ <color grey>Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)</color>\\ <color grey>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</color>
 +  - **[[https://www.lri.fr/~sboldo/files/stageM2_an.pdf|Erreurs d'arrondi en analyse numérique]]** \\ <color grey>Sylvie Boldo - Inria Saclay</color>\\ <color grey>2.7.2 2.36.1</color>
 +  - **[[http://dbweb.enst.fr/internships/probabilistic_data_msc_internship_2015.pdf|Querying Probabilitistic Data via Tree Decompositions]]** \\ <color grey>Pierre Senellart - Télécom ParisTech & National University of Singapore</color>\\ <color grey>2.26.2, 2.26.1, 2.16</color>
 +  - **[[https://www.ibisc.univ-evry.fr/~delapla/stage/canonicity-internships.pdf|Canonical form of  Boolean network & properties]]** \\ <color grey>Franck Delaplace - IBISC LAB, Tarek Melliti - IBISC LAB</color>\\ <color grey>I32, </color>
 +  - **[[http://www-pequan.lip6.fr/~tierny/stuff/openPositions/internship2014_b.html|3D Time-Traveler: Interpolation Interactive 3D+T]]** \\ <color grey>Julien Tierny _julien.tierny@lip6.fr_, Julie Delon _julie.delon@parisdescartes.fr_, Sorbonne Universites UPMC - LIP6, Paris (Metro 7,10)</color>\\ <color grey></color>
 +  - **[[http://www-pequan.lip6.fr/~tierny/stuff/openPositions/internship2015.html|inSitu Topology: Visualisation pour le Calcul Haute Performance]]** \\ <color grey>Julien Tierny _julien.tierny@lip6.fr_, Sorbonne Universites UPMC - LIP6, Paris (Metro 7, 10)</color>\\ <color grey></color>
 +  - **[[http://www-pequan.lip6.fr/~tierny/stuff/openPositions/internshipEDF_2014.pdf|Construction de graphes de Reeb et squelettes topologiques pour la visualisation des champs scalaires dans le logiciel Open-Source ParaView]]** \\ <color grey>Alejandro Ribes _alejandro.ribes@edf.fr_, Julien Tierny _julien.tierny@lip6.fr_, EDF Clamart</color>\\ <color grey></color>
 +  - **[[http://ajacs.inria.fr/internships/proxies.html|Sémantique formelle des proxies de la prochaine version de JavaScript]]** \\ <color grey>Alan Schmitt - Inria Rennes</color>\\ <color grey>2.7.2, 2.36.1</color>
 +  - **[[https://www.laas.fr/boreal/web/fr/stage/voirStage/224|Proof of convergence for a spacecraft guidance rendezvous algorithm]]** \\ <color grey>M. Joldes, C. Louembet - LAAS-CNRS, Toulouse</color>\\ <color grey></color>
 +  - **[[http://www.cea.fr/ressources-humaines/stages/les-offres-de-stage/liste-des-stages/interactions-entre-profilage-statique-et-ordonna|Interactions entre profilage statique et ordonnancement]]** \\ <color grey>Florian Brandner, ENSTA</color>\\ <color grey></color>
 +  - **[[http://www.ima.umn.edu/2014-2015/W11.10-14.14/activities/Corteel-Sylvie/corteelima9nov.pdf|Étude combinatoire d'arbres et d'arrangements d'hyperplans]]** \\ <color grey>Sylvie Corteel (LIAFA Universite Paris Diderot et David Forge (LRI, Universite Paris Sud)) corteel@liafa.univ-paris-diderot.fr, forge@lri.fr</color>\\ <color grey>C2-10</color>
 +  - **[[https://www.lri.fr/~benzaken/documents/sujetconcur.pdf|Data intensive management systems concurrency control Coq mechanization]]** \\ <color grey>V. Benzaken, É. Contejean, LRI - CNRS Orsay</color>\\ <color grey></color>
 +  - **[[http://iml.univ-mrs.fr/~beffara/stage-m2if.pdf|Étude logique de l'ordonnancement dans les algèbres de processus]]** \\ <color grey>Emmanuel Beffara - LIP, ENS Lyon</color>\\ <color grey>1.20, 2.1, 2.2, 2.3, 2.4</color>
 +  - **[[http://tabareau.fr/coqhott|Define an internalization of Homotopy Type Theory in Coq]]** \\ <color grey>N. Tabareau/M. Sozeau - Inria, Nantes-Paris</color>\\ <color grey>2.7.2</color>
 +  - **[[http://tabareau.fr/coqhott|Define and implement a general notion of higher inductive types]]** \\ <color grey>N. Tabareau/M. Sozeau - Inria, Nantes-Paris</color>\\ <color grey>2.7.2</color>
 +  - **[[http://www.loria.fr/~contasss/documents/StageENS2015.pdf|Parallel algorithms for geometric information analysis from 3D scanners]]** \\ <color grey>Sylvain Contassot-Vivier and Adrien Krähenbühl - LORIA Nancy</color>\\ <color grey></color>
 +  - **[[http://perso.ens-lyon.fr/colin.riba/sujets/mso-arith-M2-2015.pdf|Proof-Theoretic Strengh of MSO on Infinite Words]]** \\ <color grey>Colin Riba -- LIP - ENS de Lyon</color>\\ <color grey>2.16, 2.20.2</color>
 +  - **[[http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2015/micro-policies.pdf|Micro-Policies: A Framework for Verified, Tag-Based Security Monitors]]** \\ <color grey>Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)</color>\\ <color grey>2.4, 2.5.1, 2.6, 2.7.2, 2.36.1</color>
 +  - **[[https://www.rocq.inria.fr/secret/Anne.Canteaut/MPRI/stage-cea.pdf|Étude de la résistance des algorithmes de cryptographie légère face aux attaques physiques]]** \\ <color grey>Jacques Fournier - CEA LSAS, Centre Micro-électronique de Provence, Gardanne (13)</color>\\ <color grey>2.13.2 et 2.12.1</color>
 +  - **[[http://www.liafa.univ-paris-diderot.fr/~asarin/sujets/bitsPerSecond.html|Information per time unit in timed systems]]** \\ <color grey>E. Asarin and A. Degorre - LIAFA</color>\\ <color grey>2-8-2</color>
 +  - **[[http://www.liafa.univ-paris-diderot.fr/~asarin/sujets/compression.html|Compression of mixed (discrete-continuous) signals]]** \\ <color grey>E. Asarin and A. Degorre - LIAFA</color>\\ <color grey>2-8-2</color>
 +  - **[[http://perso.telecom-paristech.fr/~ware/tmp/sujet-stage-SDN.pdf|Nouvelles abstractions logicielles pour les réseaux optiques SDN]]** \\ <color grey>Cédric Ware - Télécom ParisTech</color>\\ <color grey></color>
 +  - **[[http://www.lix.polytechnique.fr/comete/stages/#om|Optimal mechanisms for the protection of confidential information]]** \\ <color grey>Catuscia Palamidessi and Konstantinos Chatzikokolakis. INRIA and Ecole Polytechnique</color>\\ <color grey></color>
 +  - **[[http://www.loria.fr/~moroz/internships/2015-master-singcast.pdf|Topology of singular curves and surfaces]]** \\ <color grey>Guillaume Moroz et Marc Pouget</color>\\ <color grey>ALGO COCA 2.22 2.13.1</color>
 +  - **[[http://www.pps.univ-paris-diderot.fr/~kesner/stages/sujet-2015a.pdf|Standardisation in the linear substitution calculus]]** \\ <color grey>Delia Kesner - PPS - Univ. Paris-Diderot</color>\\ <color grey></color>
 +  - **[[http://www.pps.univ-paris-diderot.fr/~kesner/stages/sujet-2015b.pdf|A New Operational Semantics for the Focalized Intuitionistic Sequent Calculus]]** \\ <color grey>Delia Kesner - PPS - Univ. Paris-Diderot</color>\\ <color grey></color>
 +  - **[[http://www.ssi.gouv.fr/IMG/pdf/SDE010_Analyse_de_la_securite_d_algorithmes_de_chiffrement_authentifie.pdf|Analyse de la sécurité d'algorithmes de chiffrement authentifié]]** \\ <color grey>Thomas Fuhr et Henri Gilbert - ANSSI, Paris</color>\\ <color grey></color>
 +  - **[[http://gallium.inria.fr/~xleroy/stage-2015-1.html|Verified JIT compilation of Coq]]** \\ <color grey>Xavier Leroy, Maxime Dénès -- Inria Paris-Rocquencourt</color>\\ <color grey>2-4, 2-7-1, 2-7-2</color>
 +  - **[[http://gallium.inria.fr/~fpottier/stages/sujet2015.pdf|Vérification formelle d’analyses de complexité]]** \\ <color grey>Francois Pottier et Arthur Charguéraud, INRIA Paris-Rocquencourt</color>\\ <color grey>2.4, 2.7.2, 2.36.1</color>
 +  - **[[http://nicolasperrin.net/documents/internship_proposal_perrin.pdf|A game-theoretic approach to controller synthesis for the acrobot swing-up problem]]** \\ <color grey>Nicolas Perrin - Paris</color>\\ <color grey>2.8.2, 2.20.1, 1-19, 1-22</color>
 +  - **[[http://gallium.inria.fr/~fpottier/stages/sujet2015-m2.pdf|Conception et implémentation d’un outil et d’une librairie OCaml pour manipuler les lieurs]]** \\ <color grey>Francois Pottier, INRIA Paris-Rocquencourt</color>\\ <color grey>2.4</color>
 +  - **[[http://www.lsv.ens-cachan.fr/~bouyer/files/sujet-m2-2015.pdf|Games of imperfect information over graphs]]** \\ <color grey>Patricia Bouyer (LSV), Samson Lasaulce (L2S), Nicolas Markey (LSV)</color>\\ <color grey>2.20.1, 1.22, 1.24</color>
 +  - **[[http://cedric.cnam.fr/~delahaye/docs/stage.pdf|Vérification de preuves d'arithmétique dans le lambda-Pi-calcul modulo]]** \\ <color grey>David Delahaye - Inria Paris (Place d'Italie)</color>\\ <color grey>2.5.1, 2.7.1, 2.7.2, 2.36.1</color>
 +  - **[[http://androide.lip6.fr/?q=node/77|Une approche inspirée de l'archéologie pour l'analyse de données de votes dans une élection]]** \\ <color grey>Olivier Spanjaard, Fanny Pascual - Sorbonne Universités Univ Paris 06, Laboratoire d'Informatique de Paris 6</color>\\ <color grey>Algorithmique, optimisation combinatoire, complexité</color>
 +  - **[[http://www.di.ens.fr/~mine/enseignement/mpri/2014-2015/stages/stage-M2-matrix.pdf|Static analysis by abstract interpretation of the functional correctness of vector and matrix manipulating programs]]** \\ <color grey>Antoine Miné - École normale supérieure</color>\\ <color grey>2.6</color>
 +  - **[[https://www.lri.fr/~sboldo/files/stageM2_elfic1.pdf|Analyse fonctionnelle en Coq]]** \\ <color grey>Sylvie Boldo - Inria Saclay</color>\\ <color grey>2.7.2</color>
 +  - **[[https://www.lri.fr/~sboldo/files/stageM2_elfic2.pdf|Analyse des erreurs d'arrondi d'une bibliothèque d'analyse numérique]]** \\ <color grey>Sylvie Boldo - Inria Saclay</color>\\ <color grey>2.36.1</color>
 +  - **[[http://www-poleia.lip6.fr/~bampise/mapreduce.pdf|Algorithmic issues in MapReduce]]** \\ <color grey>E. Bampis, G. Lucarelli, D. Trystram - INRIA Grenoble or LIP6</color>\\ <color grey>2.24.1, 2.29.1</color>
 +  - **[[http://www.stages.defense.gouv.fr/index.php?page=StageVisualisationPage&stage=3680&parent=DepartementPage&pc=2|conception et la programmation d'algorithmes de reconstruction de codes correcteurs d'erreurs]]** \\ <color grey>Pierre Loidreau - Direction générale de l'armement (Rennes)</color>\\ <color grey>2.13.2 </color>
 +  - **[[http://pageperso.lif.univ-mrs.fr/~pierre-alain.reynier/sujet-m2-robustness.pdf|Comparison of robustness and samplability for timed automata]]** \\ <color grey>Pierre-Alain Reynier (LIF)</color>\\ <color grey>2.8.2</color>
 +  - **[[http://pageperso.lif.univ-mrs.fr/~pierre-alain.reynier/sujet-m2-transducers.pdf|Deciding rational functions among regular ones using streaming string transducers]]** \\ <color grey>Pierre-Alain Reynier (LIF)</color>\\ <color grey>2.16</color>
 +  - **[[http://www.di.ens.fr/~vdelaitr/|Programing of an image description API]]** \\ <color grey>Vincent Delaitre</color>\\ <color grey></color>
 +  - **[[http://perso.esiee.fr/~mustafan/nabilmpri2015.pdf|Approximation Algorithms for Combinatorial Optimization Problems in Geometry]]** \\ <color grey>Nabil Mustafa - LIGM Universite Paris-Est</color>\\ <color grey></color>
 +  - **[[http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2015/fstar.pdf|F*: SMT-Based Verification for ML]]** \\ <color grey>Catalin Hritcu - Inria Paris-Rocquencourt (Place d'Italie office)</color>\\ <color grey>2.4, 2.7.2, 2.36.1, 2.5.1, 2.7.1, 2.6, 2.1</color>
 +  - **[[http://lifeware.inria.fr/wiki/jobs/#mmcmaes|Evolutionary Algorithm: Mixture-Model Extension of CMA-ES for Multi-Modal Optimization]]** \\ <color grey>François Fages - Inria Paris-Rocquencourt</color>\\ <color grey>2.24.1, 2.19</color>
 +  - **[[http://lifeware.inria.fr/wiki/jobs/#tropicalization|Tropical constraint methods for reducing biochemical reaction systems with multiple timescales]]** \\ <color grey>François Fages - Inria Paris-Rocquencourt</color>\\ <color grey>2.19, 2.13.1</color>
 +  - **[[http://lifeware.inria.fr/wiki/jobs/#multistationarity|Boucles de rétroaction positive et multistationarité dans des systèmes de réactions biochimiques]]** \\ <color grey>Sylvain Soliman - Inria Paris-Rocquencourt</color>\\ <color grey>C2.19, C2.29.1</color>
 +  - **[[http://lifeware.inria.fr/wiki/jobs/#influreac|Inférence de modèle réactionnel correspondant à un graphe d’influence]]** \\ <color grey>François Fages et Sylvain SOliman - Inria Paris-Rocquencourt</color>\\ <color grey>C2.19, C2.6</color>
 +  - **[[http://perso.esiee.fr/~mustafan/nabilmpri2015.pdf|Approximation Algorithms for Combinatorial Optimization Problems in Geometry ]]** \\ <color grey>Nabil Mustafa - LIGM Universite Paris-Est</color>\\ <color grey></color>
 +  - **[[http://lifeware.inria.fr/wiki/jobs/#inhibitors|Boolean models of biochemical reactions]]** \\ <color grey>François Fages - Inria Paris-Rocquencourt</color>\\ <color grey>C2-19, C2.6</color>
 +  - **[[http://www.lix.polytechnique.fr/~neron/Publi/mpri.pdf|Proof Engineering Tools for Coq]]** \\ <color grey>Eelco Visser and Pierre Neron and Andrew Tolmach - TU Delft - Netherlands) </color>\\ <color grey>2.7.2 2.4</color>
 +  - **[[http://www.di.ens.fr/~rival/stage-disj.pdf|Accurate and Efficient Disjunctions of Abstract Properties of Memory States]]** \\ <color grey>Xavier Rival - DIENS</color>\\ <color grey>2.6</color>
 +  - **[[http://www.di.ens.fr/~rival/stage-relation.pdf|Abstraction de Relations entre États de la Mémoire]]** \\ <color grey>Xavier Rival - DIENS</color>\\ <color grey>2.6</color>
 +  - **[[http://perso.telecom-paristech.fr/~rauzy/internship_formal-dpl.pdf|Formal Study of a Countermeasure Against Side-Channel Attacks]]** \\ <color grey>Pablo Rauzy and Sylvain Guilley, at Télécom ParisTech</color>\\ <color grey></color>
 +  - **[[http://perso.telecom-paristech.fr/~rauzy/internship_formal-eccfa.pdf|Protecting Elliptic Curve Cryptography Against Fault Injection Attacks]]** \\ <color grey>Pablo Rauzy and Sylvain Guilley, at Télécom ParisTech</color>\\ <color grey></color>
 +  - **[[https://sites.google.com/site/beniaminoaccattoli/Home/lambda-to-pi-internship|Formalizing Functions as Processes]]** \\ <color grey>Beniamino Accattoli - INRIA Saclay, Parsifal Team</color>\\ <color grey></color>
 +  - **[[http://www.di.ens.fr/~feret/stages/mpri_2014_2015_1.pdf|A weakly relational domain to detect potential polymerisation events in signaling pathways]]** \\ <color grey>J Feret, DI - Ecole normale supérieure, 75005 Paris</color>\\ <color grey>M2 - 6: Abstract interpretation</color>
 +  - **[[http://www.di.ens.fr/~feret/stages/mpri_2014_2015_2.pdf| Approximate model reduction for the differential semantics of rule-based models]]** \\ <color grey>J Feret, DI - Ecole normale supérieure, 75005 Paris</color>\\ <color grey>M2 - 6: Abstract interpretation</color>
 +  - **[[http://www.liafa.univ-paris-diderot.fr/~nschaban/2015.01.14-StageM2.pdf|Algorithmes de Partitionnement de Graphes Dynamiques - Dynamic Graphs Partitionning Algorithms]]** \\ <color grey>Nicolas Schabanel - LIAFA (U. Paris Diderot)</color>\\ <color grey>2.11.1, ,1.24, 2.11.2, 2.18.1, 2.24.1, 2.29.1, 2.38.1</color>
 +  - **[[https://github.com/mirage/mirage-www/wiki/Pioneer-Projects|Functional Programming and Operating System research]]** \\ <color grey>Thomas Gazagnaire - University of Cambridge</color>\\ <color grey></color>
 +  - **[[http://www.lix.polytechnique.fr/Labo/Emmanuel.Haucourt/uploads/teaching/directed_Gelfand.pdf|Gelfand duality for compact partially ordered spaces]]** \\ <color grey>Emmanuel Haucourt - École Polytechnique (LIX)</color>\\ <color grey>Concurrency 2.3</color>
 +  - **[[http://www.lix.polytechnique.fr/Labo/Emmanuel.Haucourt/uploads/teaching/almost_free_categories.pdf|almost free categories]]** \\ <color grey>Emmanuel Haucourt - École Polytechnique (LIX)</color>\\ <color grey>Concurrency 2.3</color>
 +  - **[[https://lama.univ-savoie.fr/~hirschowitz/stages/stage-2015/sosCat.html|Sémantique opérationnelle catégorique]]** \\ <color grey>Tom Hirschowitz - Chambéry</color>\\ <color grey>1-20;2.2;2.3</color>
 +  - **[[http://lipn.univ-paris13.fr/~guerrini/stages/proposal/CombProofSN.pdf|Strong normalisation for simply typed lambda-calculus: a quest for new combinatorial proofs]]** \\ <color grey>Stefano Guerrini, Giulio Manzonetto</color>\\ <color grey>2.1, 2.2 et 2.4</color>
 +  - **[[http://sebastien.bardin.free.fr/sujet-M2-contraintes.pdf|Résolution de contraintes pour la vérification de programmes]]** \\ <color grey>Sébastien Bardin, CEA LIST (Paris-Saclay)</color>\\ <color grey></color>
 +  - **[[http://sebastien.bardin.free.fr/sujet-M2-couverture-labels.pdf|Génération de tests structurels pour des critères avancés]]** \\ <color grey>Sébastien Bardin, Nikolay Kosmatov, CEA</color>\\ <color grey></color>
 +  - **[[http://sebastien.bardin.free.fr/sujet-M2-plateforme.pdf|Réalisation d'outils pour le décodage d'exécutables]]** \\ <color grey>Sébastien Bardin, CEA LIST (Paris-Saclay)</color>\\ <color grey></color>
 +  - **[[http://sebastien.bardin.free.fr/sujet-M2-crash.pdf|Génération automatique d'exploits à partir de traces d'erreurs]]** \\ <color grey>Marie-Laure Potet, Laurent Mounier (Verimag), Sébastien Bardin (CEA)</color>\\ <color grey></color>
 +  - **[[contact ahmed.bouabdallah@telecom-bretagne.eu|Negotiation of correspondence policies]]** \\ <color grey>A.Bouabdallah - L.Cailleux / Location = DGA/MI (Bruz) or Telecom Bretagne (Rennes)</color>\\ <color grey></color>
 +  - **[[Categorical Semantics of Distributed Version Control Systems|Categorical Semantics of Distributed Version Control Systems]]** \\ <color grey>Samuel Mimram (LIX, École Polytechnique)</color>\\ <color grey>1-20, 2.2</color>
 +  - **[[Categorical Semantics of Distributed Version Control Systems|Categorical Semantics of Distributed Version Control Systems]]** \\ <color grey>Samuel Mimram (LIX, École Polytechnique)</color>\\ <color grey>1-20, 2.2</color>
 +  - **[[http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/tmp/dvcs_cat.pdf|Categorical Semantics of Distributed Version Control Systems ]]** \\ <color grey>Samuel Mimram (LIX, École Polytechnique)</color>\\ <color grey>1-20, 2.2</color>
 +  - **[[http://pagesperso-systeme.lip6.fr/Swan.Dubois/pdf/sujet1.pdf|Enabling clusters with Dynamic Distributed Systems]]** \\ <color grey>Franck Petit, Swan Dubois, UPMC/Inria</color>\\ <color grey>2.18.1</color>
 +  - **[[http://pagesperso-systeme.lip6.fr/Swan.Dubois/pdf/sujet2.pdf|Validation of distributed protocols for opportunistic networks]]** \\ <color grey>Franck Petit, Swan Dubois, UPMC/Inria</color>\\ <color grey>2.18.1</color>
  
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA