Submit an internship offer

1. Analyse statique de programme par interprétation abstraite
   David Monniaux, Grenoble
   2.6, 2.9.2, 2.5
2. Analyse modulaire de programmes
   David Monniaux, Grenoble
   2.6, 2.9.2, 2.5
3. Analyse de programme efficace : SMT-solving et itérations
   David Monniaux, Grenoble
   2.6, 2.9.2, 2.5
4. Optimisation de formules SMT
   David Monniaux, Grenoble
   2.5
5. Décision de formules contenant des flottants
   David Monniaux, Grenoble
   2.5
6. Techniques de compilation dédiées pour un langage spécifique à un domaine (SystemC)
   Matthieu Moy, Verimag, Grenoble
   
7. Performance Evaluation for Embedded Systems using Formal Methods
   Matthieu Moy et Karine Altisen, Verimag, Grenoble
   
8. Réduction de modèles à plusieurs échelles de temps en tant que réécriture de graphe
   Ovidiu Radulescu / Biophysique théorique et biologie des systèmes, DIMNP UMR 5235, Montpellier
   éventuellement, 2.19 & 2.6
9. Model-Checking Techniques for Virus and Malware Detection
   Tayssir TOUILI - LIAFA, Paris
   1-22, 2.6, 2.9.1, 2.9.2
10. Strategy hybridation for normative conflict resolution
    Guillaume Piolle & Valérie Viet Triem Tong - Supélec, Rennes, France
    Automated deduction, proof systems, proof assistants
11. Implementing the right to be forgotten
    Sébastien Gambs & Guillaume Piolle - Supélec, Rennes
    
12. Gathering Entropy from Solid State Drives
    Guillaume Salagnac - CITI INSA-Lyon
    
13. Fusion de Données d’une Console KINECT et de Capteurs additionnels
    Fabrice Michel
    
14. Hachage parfait pour la compression de données
    Fabrice Michel - Dassault Systemes Vélizy
    
15. Economics of privacy in social networks
    Patrick Loiseau - EURECOM (Sophia-Antipolis)
    
16. Resource allocation in data centers: reliability vs energy consumption
    Patrick Loiseau - EURECOM (Sophia-Antipolis)
    
17. Interaction between game theory and statistical learning: the example of a spam filter
    Patrick Loiseau - EURECOM (Sophia-Antipolis)
    
18. Kleene algebras, automata and regular expressions
    Damien Pous - ENS Lyon
    
19. PiCoq: pi-calculus within Coq
    Damien Pous - ENS Lyon
    
20. Decision procedures for cyclic linear logic and non-commutative structures.
    Damien Pous - ENS Lyon
    
21. Homological simplification for reconstruction
    Marc Glisse - INRIA Saclay (Polytechnique)
    
22. Approche polyédrale pour le problème de planification des démarrages d'unités de production
    C.Dürr, LIP6
    2-24-1
23. Ordonnancement robuste de tâches pour la maintenance d'une unité de production d'électricité
    Pierre Fouilhoux, LIP6
    2-24-1
24. Cryptanalyse AES
    Pierre-Alain Fouque (IRISA/RENNES)
    Crypto
25. Generalisations des matrices a signes alternants
    Sylvie Corteel - LIAFA (175 rue du Chevaleret Paris)
    C2-10, C2-15
26. Frontière entre décidabilité et indécidabilité pour la finitude de groupes d'automates.
    Ines Klimann, LIAFA (Université Paris Diderot)
    2.16, 2.20.2
27. ALGORITHMIQUE DES GRAPHES PLONGÉS SUR DES SURFACES: dessin de graphes
    Luca Castelli Aleardi, Eric Fusy (LIX, Ecole Polytechnique)
    2.38.1, 2.10
28. Structures de données compactes pour les maillages
    Luca Castelli Aleardi, Gilles Schaeffer (LIX, Ecole Polytechnique)
    2.38.1, 2.10
29. Reachability in Lossy VASS
    Sylvain Schmitz - LSV, ENS Cachan
    2.9.1
30. VASS Simulations
    Sylvain Schmitz - LSV, ENS Cachan
    2.9.1
31. Tracelet Semantics of Weak Memory
    Jade Alglave and Peter O'Hearn - London
    
32. Links between AI and Program Verification
    Peter O'Hearn and Jules Villard
    
33. Hardware-based Privilege Separation for Cryptographic Protocol Implementations
    Karthikeyan Bhargavan and Graham Steel
    2.30, 2.36.1
34. Coinductive algorithms for non standard automata
    Damien Pous - Filippo Bonchi
    
35. State-Space Reductions for Verifying Equivalences of Security Protocols
    David Baelde and Stéphanie Delaune - LSV / ENS Cachan
    2.30 / 2.3
36. Verification of security protocols: composition issues
    Véronique Cortier and Stéphanie Delaune - Nancy and/or Cachan
    2.30
37. Verification of equivalence properties in security protocols
    Stéphanie Delaune and Steve Kremer - Cachan and/or Nancy
    2.30
38. Formalizing some combinatorial attacks in security protocols
    Stéphanie Delaune and Steve Kremer - Cachan and/or Nancy
    2.30
39. Better Approximations of VASS Reachability Sets
    Alain Finkel, Jérôme Leroux
    
40. Algorithmics of infinite Downward-Closed Sets for WSTS
    Alain Finkel
    
41. Développement d’un outil de transformation de modèles
    David Lesens - Astrium Les Mureaux
    
42. Mise en oeuvre de l'outil de modélisation SCADE en conditions opérationnelles
    Sébastien Poirieux - Astrium Les Mureaux
    
43. Atelier de validation SCADE pour autocoding Ada
    Olivier Boudillet - Astrium Les Mureaux
    
44. Aide au prototypage rapide de logiciels embarqués critiques
    Christophe Goarin - Astrium Les Mureaux
    
45. Model Based Testing
    Albert Jou - Astrium Les Mureaux
    
46. Etude des réseaux Time Triggered Ethernet et AFDX
    Pierre Sautereau - Astrium Les Mureaux
    
47. Prototypage virtuel d’une architecture numérique
    Benjamin Disson - Astrium Les Mureaux
    
48. Machines de Mealy et problème de Burnside
    Matthieu Picantin, LIAFA (Université Paris Diderot)
    2.16 & 2.20.2
49. Tropicalisation
    François Fages - Inria Rocquencourt
    C2-19 C2-29-1 C2-9.1
50. Patterns of quantitative temporal logic formulae for systems biology
    François Fages - Inria Rocquencourt
    C2-19 C2.9.1
51. Computing Subgraph Epimorphisms by a Randomized Adaptive Search Procedure
    François Fages - Inria Rocquencourt
    C2-24-1 C2-29-1 C2-19 C2-10
52. Le diamètre du multiassociaèdre
    Vincent Pilaud & Lionel Pournin - LIX, École Polytechnique
    2.10
53. Multitriangulations de surfaces
    Vincent Pilaud - LIX, École Polytechnique
    2.10, 2.38.1
54. Diffusion chiffrée avec décentralisation de la gestion des membres
    David Pointcheval - ENS
    Cryptographie
55. Algorithmes de recherche des bassins d’attraction dans des graphes de modélisation des systèmes dynamiques complexes
    Olivier Roux IRCCyN, Ecole Centrale de Nantes — Equipe MeForBio
    2.19 (souhaitable); 2.6 (éventuellement)
56. Around a new algorithm to solve systems of linear equations modulo p
    Charles Bouillaguet — LIFL Lab (Lille)
    calcul formel, algorithmes randomisés, algorithmes pour la crypto
57. Réduction de modèles à plusieurs échelles de temps en tant que réécriture de graphe
    Ovidiu Radulescu / Biophysique théorique et biologie des systèmes, DIMNP UMR 5235, Montpellier
    éventuellement, 2.19 & 2.6
58. Réduction de processus de frappe via leur sémantique différentielle
    Olivier Roux: IRCCyN, Ecole Centrale de Nantes - Equipe MeForBio & Ovidiu Radulescu: Biophysique théorique et biologie des systèmes, DIMP UMR 5235, CNRS/Université de Montpellier 1&2
    éventuellement, 2.19 & 2.6
59. Optimisation du chiffrement homomorphe
    N. El Mrabet and N. Gama - PRISM _ Université de Versailles
    2.12.1, 2.12.2
60. Définition d'un modèle temporisé du langage AltaRica.
    Antoine RAUZY, Michel BATTEUX, Tatiana PROSVIRNOVA - LIX Polytechnique
    
61. Tableaux et raisonnement arithmétique dans le compilateur Mezzo
    François Pottier, INRIA Paris-Rocquencourt
    2.4, 2.36.1
62. Etude de la sécurité d’un mécanisme générique de délégation de calculs cryptographiques
    Sébastien Canard - Orange Labs Caen
    1.1; 1.13; 1.14; 1.22; 2.7.2; 2.12.1; 2.12.2; 2.22; 2.30
63. Bisimulations pour le calcul de réécriture
    Sergueï Lenglet - LORIA
    
64. Vérification formelle d'un calcul multiprécision de pi
    Sylvie Boldo et Guillaume Melquiond - Orsay
    2.7.1, 2.7.2, 2.22, 2.36.1
65. Limites continues d’automates cellulaires
    Julien Cervelle - Créteil
    2.33.1
66. Pavages, flips et motifs interdits
    Olivier Bodini, Thomas Fernique - Université Paris 13
    1.24, 2.15
67. Compilation de programmes réactifs
    Louis Mandel – ENS
    2.23.1, 2.4
68. Lier dynamique des maladies infectieuses et phylogénie
    Samuel Alizon (CR CNRS, MIVEGEC) & Olivier Gascuel (DR CNRS, LIRMM)
    
69. Interference abstractions for thread-modular static analyses by abstract interpretation
    Antoine Miné - École normale supérieure, Paris
    M2-6
70. Sémantique et formule de Taylor
    Thomas Ehrhard, Christine Tasson, PPS Paris
    2.1,2.2
71. Invariants of proofs in classical logic
    Lutz Strassburger – INRIA Saclay
    
72. Counting Proof Nets
    Lutz Straßburger – INRIA Sacalay
    
73. Déduction automatique modulo
    David Delahaye, Damien Doligez, et Olivier Hermant - Inria Paris
    2.5, 2.7.1, 2.7.2, 2.36.1
74. Sémantiques de jeux concurrentes
    Tom Hirschowitz - Chambéry
    1-15,1-20,2-1,2-2,2-3
75. Axiomatisation d'équivalence de programmes en Coq
    Alan Schmitt - Inria Rennes
    2.3, 2.4, 2.7.2, 2.36.1
76. Sémantique des obfuscations de programmes
    Sandrine Blazy - INRIA Rennes
    2.4 2.7.2
77. Traduction et extension d’un langage de description des protocoles de sécurité vers une algèbre de réseaux de Petri
    Frédéric Gava and/or Franck Pommereau
    
78. Certification en Coq d'une implantation distribuée de squelettes de flots.
    Frédéric Gava and/Joel Falcou
    
79. Une bibliothèque applicative (parallèle) d'algorithmes BSP sur les graphes; implantation générique et expérimentations.
    Frédéric Gava
    
80. Statistical Aspects of Topologigal Data Analysis
    Frédéric Chazal - INRIA Saclay (Bat. Turing, Campus de l'Ecole Polytechnique)
    
81. Complexité de communication et langages d'images
    Emmanuel Jeandel - LORIA (Nancy)
    Fondations mathématiques de la théorie des automates, Théorie des calculs
82. Clustering with noisy multiplex data
    Claire Mathieu - DI ENS
    
83. Translation validation for synchronous data-flow equations in a Lustre compiler
    Francesco Zappa Nardelli, Marc Pouzet, École normale supérieure
    
84. Compilation of Zero-crossing Detection in Languages for Hybrid Systems
    Marc Pouzet, Timothy Bourke — École normale supérieure
    
85. Extending Synchronous Languages with Oracles
    Marc Pouzet, École normale supérieure
    
86. Nearest Neighbour Searching
    Mariette YVINEC-INRIA Sophia Antipolis
    2-14-1
87. Rewriting methods for homology computation
    Pierre-Louis Curien / Yves Guiraud / Philippe Malbos / Samuel Mimram - PPS (Université Paris 7) / CEA Saclay
    2.2 (modèles de langages de programmation), 2.4 (programmation fonctionnelle)
88. Moving focusing proof systems to arithmetic
    Dale Miller, LIX & INRIA-Saclay
    2.1, 2.7.1, 2.7.2
89. codes localement décodables et applications aux calculs déportés et au stockage distribué
    Françoise Levy-dit-Vehel and Daniel Augot
    2-13-2
90. Abstraction de relations entre états mémoire
    Xavier Rival - DIENS
    2.6
91. Analyse statique de programmes manipulant des structures de données complexes avec partage
    Xavier Rival - DIENS
    2.6
92. Geometry and topology of curves: a symbolic numeric approach
    Marc Pouget et Guillaume Moroz
    2.22 2.13.1
93. Sécurité des systèmes : mesures de l'opacité et des fuites d'information
    B.Bérard, J. Mullins LIP6, UPMC et Ecole Polytechnique de Montréal
    1-24 et 2.9.2
94. Random generation of combinatorial objects
    Ana Busic and Anne Bouillard - INRIA and ENS, Paris
    2.10, 2.15, 2.17.1
95. Renewable Energy and the Smart Grid
    Ana Busic
    2.17.1, 2.24.1
96. Interprétation fonctionnelle des systèmes de réécriture de mots (non associatifs)
    Laurent Poinsot - LIPN, Université Paris 13
    
97. Graphes de permutation circulaire et problèmes d'optimisation et dimension d'ordre
    V. Limouzy - Limos - Clermont-Ferrand
    2.29.1
98. Temporal logics with energy constraints
    Patricia Bouyer, Nicolas Markey (LSV, Cachan)
    2.8,2.20.1
99. Nash equilibria in multiplayer infinite-state games
    Patricia Bouyer, Nicolas Markey (LSV, Cachan)
    2.8,2.20.1
100. Mixed Nash equilibria in multiplayer concurrent games
     Patricia Bouyer, Nicolas Markey (LSV, Cachan)
     2.8,2.20.1
101. Filtrage et modèles de termes
     Vincent Padovani - PPS (Paris Diderot)
     
102. Vérification formelle d’implémentations cryptographiques
     Quang-Huy Nguyen - Versailles
     2.4, 2.4, 2.9.2, 2.12.1, 2.12.2
103. Génération de graphes de dépendances de programmes modulaires
     Boris Yakobowski - CEA LIST (Saclay)
     2.6, 2.92
104. Connexité dans les grands graphes
     David Coudert – Mascotte, INRIA, I3S, CNRS, Univ. Nice Sophia (Sophia Antipolis)
     
105. Méthodes catégoriques pour la modélisation et la vérification d’architectures
     David Chemouil, Julien Brunel - Onera Toulouse
     
106. Un langage de programmation pour le contrôle des architectures logicielles à l’exécution
     David Chemouil, Julien Brunel - Onera Toulouse
     
107. Graphs with low forwarding index and few extra edge
     Stephane Perennes and Frederic Giroire – Mascotte, INRIA, I3S, CNRS, Univ. Nice Sophia (Sophia Antipolis)
     
108. Fractional Cops and Robber Games
     Stephane Perennes and Ronan Pardo Soares – Mascotte, INRIA, I3S, CNRS, Univ. Nice Sophia (Sophia Antipolis)
     
109. Calculs de centres et de diamiètre d'un graphe
     Michel Habib, LIAFA
     
110. Pavages, assemblage et motifs interdits
     Olivier Bodini, Thomas Fernique
     1.24, 2.15
111. Pavages, assemblage et motifs interdits
     Olivier Bodini, Thomas Fernique - Université Paris 13
     1.24, 2.15
112. The "Red Stone Model": a cellular automaton with conservation rules
     A. Sportiello – LIPN, Univ. Paris 13
     2.10, 2.15
113. Combinatoire des pavages par dominos
     Sylvie Corteel et Jeremi Bouttier - LIAFA Universite Paris Diderot
     C2-10, C2-15
114. The Linux Memory Model
     Francesco Zappa Nardelli - ENS Paris
     2.37.1, 2.36.1
115. Rétro-ingénierie de ligne de produits logiciels depuis le code source
     Yves Le Traon (Université de Luxembourg), Tewfik Ziadi (LIP6)
     
116. Transcription rythmique
     Jean Bresson, Florent Jacquemard - Ircam
     2.16
117. Reconstruction de graphe par un agent mobile disposant d'une vue locale
     Jérémie Chalopin, LIF, Marseille
     
118. Programmation parallèle synchrone pour GPUs et accélérateurs matériels
     Albert Cohen
     2.37.1, 2.23.1
119. Algorithmes approchés pour la recherche de k plus courts chemins dans des graphes acycliques, planaires et orientés : Application à la recherche de microARNs dans les génomes
     Eric Angel (équipe OPAL) et Fariza Tahi (équipe AMIS), du laboratoire IBISC. Laboratoire IBISC, IBGBI, Université d'Evry, 23 Boulevard de France, 91000 Evry.
     
120. Analysis of advanced travel search engines based on graph
     Eric Madelaine - David Coudert, INRIA Sophia-Antipolis
     Algorithmique distribuée pour les réseaux; Algorithmique des graphes
121. Domaines abstraits pour l'analyse de programmes avec mémoire dynamique
     Constantin Enea & Mihaela Sighireanu, LIAFA
     2.9.2, 2.6
122. Efficient Data Structures for Next-Generaton Sequencing Data
     LIGM, Marne-la-Vallée
     Algorithmique, Algorithmique avancée
123. Efficient Data Structures for Next-Generaton Sequencing Data
     Gregory Kucherov - LIGM, Marne-la-Vallée
     Algorithmique, Algorithmique avancée
124. Sur la sémantique des programmes auto-modifiants
     Jean-Yves Marion
     
125. Unification de deux méthodes d'abstraction de données
     Franck Pommereau, Francesco Belardinelli
     
126. Simulation rapide de réseaux de Petri colorés
     Franck Pommereau
     
127. Méthode de tableaux pour le model-checking de la logique ATL
     Franck Pommereau
     
128. Privacy protection in log analysis
     Kostas Chatzikokolakis, Catuscia Palamidessi (Ecole Polytechnique and INRIA)
     2.3 (concurrency)
129. Preuve de programmes avec lieurs
     Claude Marché, Andrei Paskevich - Université Paris-sud (LRI et INRIA Saclay)
     2-36-1, 2-5, 2-7
130. Réalisabilité des spécifications en logique temporelle épistémique.
     Catalin DIMA, LACL, Université Paris-Est Créteil
     
131. Synthese d'ensemble invariant maximal pour systemes a commande commutee { Application a l'electronique de puissance
     L. Fribourg, E. Goubault - LSV, ENS Cachan
     
132. Verification of concurrent programs under relaxed memory models
     Ahmed Bouajjani - LIAFA, Univ Paris Diderot
     2.9.2, 2.3, 2.9.1
133. Classification de tâches pigmentaires sur des images multi-spectrales de zones de peau : aide au dépistage de carcinomes de la peau
     GREYC UMR CNRS 6072 , CAen
     
134. Apprentissage profond pour l’évaluation de la qualité d’images avec référence
     GREYC UMR CNRS 6072, Caen
     
135. Phénomènes de diffusion dans les réseaux
     Matthieu Latapy, LIP6 (CNRS - UPMC), Paris
     
136. Un radar pour l'internet
     Clémence Magnien - LIP6 (CNRS, UPMC) - Paris
     
137. Modélisation des graphes de terrain
     Fabien Tarissan - LIP6 (CNRS, UPMC) - Paris
     
138. Dynamiques des graphes de terrain
     Clémence Magnien - LIP6 (CNRS, UPMC) - Paris
     
139. Détection d'événements et/ou d'anomalies dans les dynamiques de graphe
     Matthieu Latapy - LIP6 (CNRS, UPMC) - Paris
     
140. Cœurs de communautés
     Jean-Loup Guillaume
     
141. La solvabilité dans le cadre des langages avec motifs
     Antonio Bucciarelli et Delia Kesner - PPS, Bâtiment Sophie Germain, 5 rue Thomas Mann. 75205 Paris CEDEX 13
     
142. Protocoles de découvertes pour WAN
     Julien Enoch - Orsay
     
143. Décomposition modulaire approchée
     Michel Habib, LIAFA -université Paris Diderot
     
144. Online search problems under new performance measures
     Spyros Angelopoulos-Paris 6
     2.24.1
145. Competition in Dynamic Social Networks
     Marc Lelarge and Alonso Silva - LINCS, Paris
     
146. Verification par Model-checking de TSAR
     LIP6 - Y. Thierry-Mieg & E. Encrenaz
     
147. Intégration et visualisation de données liées sur un référentiel géographique
     Nathalie Abadie, Fayçal Hamdi - Saint-Mandé (métro : station Saint Mandé, ligne 1)
     
148. http://www-polsys.lip6.fr/~jcf/Teaching/StageM2v2.htm
     JC Faugere et P Serre
     2-13-1
149. Modélisation de mécanismes et Algorithmes incrémentaux de Calcul des Bases de Gröbner
     JC Faugere et P Serre
     2-13-1