if-stages [Master Informatique - Université de Bordeaux]

Outils pour utilisateurs

Outils du site


if-stages

Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentesRévision précédente
Prochaine révision
Révision précédente
if-stages [2020/12/15 15:02] vpenelleif-stages [2022/01/21 13:16] (Version actuelle) vpenelle
Ligne 1: Ligne 1:
 ==== Stages de master 2 ==== ==== Stages de master 2 ====
  
-Le semestre de printemps du M2 est entièrement dévolu à un stage qui peut-être soit un stage de recherche dans un laboratoire (en France ou à l’étranger), soit un stage en entreprise. Ce stage compte pour 30ECTS et doit être vu comme une première intégration dans le type d’emploi qui souhaite être poursuivi. Ainsi, un étudiant qui souhaite poursuivre en thèse sera fortement encouragé à faire un stage en lien avec la thèse envisagée (si thèse CIFRE, le stage peut être dans l’entreprise qui co-encadrera la thèse). +Le semestre de printemps du M2 est entièrement dévolu à un stage qui peut-être soit un stage de recherche dans un laboratoire (en France ou à l’étranger), soit un stage en entreprise. Ce stage compte pour 24ECTS et doit être vu comme une première intégration dans le type d’emploi qui souhaite être poursuivi. Ainsi, un étudiant qui souhaite poursuivre en thèse sera fortement encouragé à faire un stage en lien avec la thèse envisagée (si thèse CIFRE, le stage peut être dans l’entreprise qui co-encadrera la thèse).  
 + 
 +Le stage doit durer au moins 17 semaines (contrainte du master), mais nous conseillons largement qu’ils durent au minimum 5 mois (particulièrement pour les stages de recherche, pour lesquels c’est assez crucial). À ce titre, il est conseillé de le faire démarré dès que possible (le mois d’août étant en général chômé dans les labos). Le cours d’anglais se terminant fin février, il est possible de démarrer les stages dès mars. 
 + 
 +==== Procédure coté Bordeaux ==== 
 + 
 +Une fois que vous avez un stage, il faut établir votre convention (qui doit être validée avant le départ en stage). 
 +Pour cela il y a plusieurs étapes de préparation à la convention : 
 + 
 +  - Me transmettre le sujet de stage pour que je le valide (i.e., que je vérifie que c’est un sujet adapté pour un stage de M2). Pour ça vous m’envoyez un [[vincent.penelle@u-bordeaux.fr | mail]] avec votre sujet de stage. 
 +  - Transmettre ma validation au secrétariat ainsi que les pièces suivantes : 
 +    * la [[https://www.u-bordeaux.fr/content/download/18829/141736/version/47/file/FICHE%20DE%20LIAISON%20LPRO%20MASTERS%20-%202021-2022.pdf | fiche de liaison]] 
 +    * Le récapitulatif ENT (récapitulatif éditable depuis son ENT dans un espace dédié aux stages) 
 +    * Une attestation d’assurance responsabilité civile. 
 + 
 +Évidemment, vous pouvez commencer à remplir les documents du point 2 en parallèle de mon accord (voire vous envoyez le tout au secrétariat et moi, et je donne mon accord par retour de mail). 
 + 
 +Vous pourrez trouver plus de détail sur la procédure complète [[https://www.u-bordeaux.fr/Profils/Etudiant/College-Sciences-et-technologies2/Stage/Obtenir-une-convention-de-stage | ici]].
  
 === Stages académiques === === Stages académiques ===
Ligne 37: Ligne 54:
  
  
-=== Offres 2020-2021 reçues === +=== Offres 2021-2022 reçues ===
- +
-Suit une liste d’offres reçue pour l’année 2020-2021 (que je tenterai de tenir à jour, et qui concernera sans doute les stages en entreprises, mais pas que). +
- +
-=== Académiques === +
- +
-== Équipe MF == +
- +
-Vous pouvez trouver [[https://www.labri.fr/perso/gimbert/M2/|ici]] une liste des stages proposés dans l’équipe MF du Labri. Certains d’entre eux sont également notés plus bas (si on me les a communiqués avant le lien présent. +
- +
-== Stage puis thèse à Lyon (traces d’exécutions et inférences de schémas de compilations polyédriques) == +
- +
-Dans le cadre de l'action exploratoire Inria Polytrace, un stage de M2 et une bourse de thèse sont à pourvoir dans l’équipe CASH (LIP) +
-à l’Ecole Normale Supérieure de Lyon. +
- +
-L’objectif principal de ce projet est d'exploiter statiquement des traces d'exécutions pour inférer des schémas de compilation polyédriques. +
- +
-Une description détaillée, ainsi que les informations pour postuler, sont disponibles à l’adresse suivante : +
- +
-http://perso.ens-lyon.fr/christophe.alias/polytrace.pdf +
- +
-N'hésitez pas à me contacter pour toute information complémentaire. +
- +
-Christophe Alias +
-Chargé de recherche HDR +
-Inria/ENS de Lyon +
-http://perso.ens-lyon.fr/christophe.alias +
- +
-== Stage au LaBRI == +
- +
-[[https://www.labri.fr/perso/vpenelle/Enseignement/StagesOffres/sujetTestDNN.pdf|Sujet ici]] +
- +
-Titre : Testing Deep Neural Network +
- +
-Domaine : vérification et apprentissage. +
- +
-Encadrant : Antoine Rollet. +
- +
-== Autre stage au LaBRI ==  +
- +
-Titre: De la synthèse de programmes aux tests, et vice-versa. +
- +
-Encadrants: Nathanaël Fijalkow et Antoine Rollet (LaBRI) +
- +
-Résumé: Ce stage propose d’étudier le problème de la synthèse de programme en s’inspirant de techniques de tests de programmes, et réciproquement, d’utiliser la synthèse pour faire du test. +
- +
-[[https://www.labri.fr/perso/rollet/sujets/sujetDNNvsTest.pdf|Sujet détaillé]] +
- +
- +
-Mots-clés: synthèse de programme, apprentissage, test +
- +
-Financement non acquis.  +
- +
-== Stage au Limos (Clermont-Ferrand) == +
- +
-Titre: Maintenance de décomposition de graphes. +
- +
-Encadrants: Mamadou M. Kanté et Bruno Guillon +
- +
-Résumé: Le stage concerne la maintenance de propriétés (i.e. largeur arborescente) d’un graphe lorsqu’on le modifie (ajout/retrait de sommets ou d’arêtes), et à la complexité de maintenir ces propriétés. +
- +
-Mots clés: logique ; algorithmique dynamique; Dyn-FO; MSO; base de données; graphes +
- +
-Poursuite en thèse possible. +
- +
-[[https://fc.isima.fr/~kante/cours/sujet-master-20.pdf|Sujet Détaillé]]  +
- +
- +
- +
-== Stage à Inria Bordeaux == +
- +
-Title: Design of an Interactive Demo on Multi-task Deep Reinforcement Learning using Procedurally Generated Environments +
- +
-Encadrants : Pierre-Yves Oudeyer et Rémy Portelas +
- +
-Domaine : apprentissage par renforcement. +
- +
-Stage à forte componsante ingéniérie et notamment développement web. +
- +
-[[https://www.labri.fr/perso/vpenelle/Enseignement/StagesOffres/interactiveDemoDeepRL21.pdf|Sujet Détaillé]] +
- +
-== Stage à Marseille ==  +
- +
-UN DEMONSTRATEUR POUR LA LOGIQUE DE LA CAPABILITÉ (ABILITY LOGIC) +
- +
-La logique de la capabilité (ability logic) de Elgesem est une logique +
-modale qui formalise la notion de "faire en sorte que"+
-Elle a été étudiée dans le contexte du raisonnement juridique et en +
-intelligence artificielle  dans le cadre du raisonnement multi-agent. +
-Cette logique contient deux modalités [E] et [C] indexées par des +
-agents: une  formule [E] _i A est interprété comme «l'agent i fait +
-en sorte que A», tandis que une formules [C] _i A est interprété comme +
-«l'agent i a la capacité de faire en sorte que A». +
-Dans cette logique, nous pouvons exprimer des phrases comme «John fait +
-en sorte que le loyer soit payé» - ce qui signifie à peu près +
-que John paie le loyer - et «John a la capacité de faire en sorte que le +
-loyer soit payé» - ce qui signifie à peu près que John peut payer +
-le loyer. Dans cette logique, les agents sont censés "faire en sorte +
-que" quelque chose seulement s'ils sont directement responsables +
-de sa réalisation. Par exemple, affirmer que "John fait en sorte que Bob +
-fait en sorte que le loyer soit payé" (délégation) +
-n'est pas équivalent à affirmer que John paie le loyer.  De même, un +
-agent ne peut "faire en sorte que" quelque chose qui serait +
-toujours réalisée (ou vraie), même sans son intervention : par exemple, +
-John "ne peut faire en sorte que" la terre tourne autour du soleil. +
- +
-L'objectif de cette stage est de développer un démonstrateur qui vérifie +
-si une formule de logique de Elgesem est valide ou pas +
-en produisant une preuve ou un contre-modèle.  Le démonstrateur sera +
-développé en Prolog et implémentera les calculs à hyperséquents définis +
-récemment. +
- +
-PREREQUIS : +
-Le candidat doit être en M2 d'un master en Informatique, ou en +
-Mathématiques, ou en Philosophie dans un cursus spécialement orienté à +
-la logique. +
-Des connaissances de base de la logique, et des logiques modales en +
-particulier,  des méthodes des preuves  et de la programmation logique +
-sont fortement souhaitées. +
- +
-DEBUT prévu: 1/02/2021 +
- +
-DUREE : de 4 à 5 mois +
- +
-GRATIFICATION : la gratification préconisée par la loi (actualisée pour +
-2021) pour les stages au sein d'établissements publics. +
- +
-CANDIDATURE +
-Envoyer un CV, vos relevés de notes des deux dernières années et une +
-lettre de motivation. +
- +
-CONTACTS : +
-Charles Grellois, LIS, Univ. d'Aix-Marseille, charles.grellois@univ-amu.fr +
-Nicola Olivetti, LIS, Univ. d'Aix-Marseille, nicola.olivetti @univ-amu.fr +
- +
-== Thèse à Londres == +
- +
-Proposition de doctorat à Londres. Contactez-les éventuellement pour un stage si vous êtes intéressés. +
- +
-Contact: [[p.gardner@imperial.ac.uk]] et [[t.carbajo-garcia@imperial.ac.uk]] en copie. +
- +
-Mots clés: vérification, concurrence, systèmes distribués. +
- +
-I am looking for one or two PhD students, start date in October 2021, to join my Verified Software research group. A summary of  possible research projects is given below.  +
- +
-The deadlines to apply for a PhD position in the Department are 8th January 2021 and 19th March 2021. The Department advises all students requiring funding to apply by the January deadline, although there may still be some funding available for applications received after January. Further details can be found here.  A successful UK student will probably be funded through the standard Departmental competition for funds. A successful EU/overseas student +
-will probably be funded by a combination of Departmental funding and my funding. In particular, I have additional funding which means that the EU/overseas students are able to go into the same competition for funding as the UK students. +
- +
-Please do not hesitate to  contact me directly  if interested, cc’ing my administrator Teresa Carbajo Garcia, t.carbajo-garcia@imperial.ac.uk.  +
- +
- +
-Research in the Verified Software Group, Imperial +
- +
-My group is involved with a wide range of theoretical and practical projects on symbolic testing and verification in particular, and on formal methods in general. They are summarised below.  All have many opportunities for PhD projects. +
- +
-Gillian: a multi-language platform for compositional symbolic analysis +
- +
-The Verified Software Group has recently introduced Gillian [1], a multi-language platform for compositional symbolic analysis. It currently supports three flavours of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It is underpinned by a core symbolic execution engine, parametric on the memory model of the target language, with strong mathematical foundations that unifies +
-symbolic testing and verification. Gillian has been instantiated to C and JavaScript, obtaining results on real-world code that demonstrate the viability of our unified, parametric approach. +
- +
-Possible projects include: incorporating ideas from incorrectness separation logic to Gillian [2]; extending Gillian with events and concurrency [3]; underpinning Gillian with Coq certification; +
-instantiating Gillian with C (we have just started, [1]) and Rust (we have hardly begun); and using the Gillian instantiations for symbolic testing and verification of real-world programs. +
-  +
-Concurrency +
- +
-The Verified Software Group has worked on compositional reasoning about concurrent programs, introducing fundamental techniques underpinning modern concurrent separation logics [4]: logical abstraction; logical atomicity; and logical environment liveness +
-properties. We have applied our reasoning to verify some of the most advanced concurrent algorithms. +
- +
-There is still much to understand: for example, working with the fundamental theory; applying the work to real-world libraries; developing prototype analysis tools; or moving to the Coq-focused Iris project, whose foundations use some of our theory. +
-  +
-Distribution +
- +
-The Verified Software Group has recently begun to work on weak consistency models for distribution, developing an interleaving operational semantics for client-observational behaviour of atomic transactions [5]. +
-  +
-We would be interested in finding someone to work in this area: for example, developing further the operational semantics and providing prototype tools to prove robustness results and discover litmus tests; or creating a program logic for distributed atomic transactions (our original motivation for the work) inspired by our previous work on program logics for concurrency. +
-  +
-References +
- +
-[1] Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose Fragoso Santos, Peter Maksimovic, Sacha-Elie Ayoun and Philippa Gardner, PLDI'2020. Part 2 on verification and bi-abduction is being written now! We are giving a talk on Gillian at the conference Rebase, +
-associated with ECOOP and OOPSLA, on 16th and 17th November, and at  Facebook's Testing and Verification Symposium (FaceTAV),  in December 2020.  +
- +
-[2] Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic, Azalea Raad (Imperial), Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn and Jules Villard, CAV'20. +
- +
-[3] A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications, Gabriela Sampaio, Jose Fragoso Santos, Petar Maksimovic and Philippa Gardner, ECOOP'20 +
- +
-[4] A Perspective on Specifying and Verifying Concurrent Modules, Thomas Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner, Journal of Logical and Algebraic Methods in Programming, 2018 +
- +
-[5] Data Consistency in Transactional Storage Systems: a Centralised Approach, Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP'20 +
- +
-== Stage en vérification d’essaim de robots (Lyon) == +
- +
-Des stages de niveau M2 sont proposés au sein du projet SAPPORO +
-consacré à la vérification formelle pour les essaims de robots +
-mobiles. Ces stages s'appuient sur le cadre formel Pactole. +
- +
-Le projet       --> https://sapporo.liris.cnrs.fr +
-Les offres      --> https://sapporo.liris.cnrs.fr/positions +
-Le cadre formel --> https://pactole.liris.cnrs.fr +
- +
-Les laboratoires : +
-* LIRIS/Lyon1, +
-* LIP6/Sorbonne-Université, +
-* Cedric/CNAM, +
-* DDS/Tokyo-Tech +
- +
- +
-=== Stages Mixtes Entreprise - Recherche === +
- +
-== Stage -- avec débouché en thèse potentiel -- à Thalès ==  +
- +
-[[https://www.labri.fr/perso/vpenelle/Enseignement/StagesOffres/Stage-SE-Fuzzing.pdf|Sujet ici]] +
- +
-Titre : Couverture de code à l’aide de fuzzing et d’exécution symbolique +
- +
-Domaine : vérification. +
- +
-Encadrant : Nikolai Kosmatov (CEA Saclay). +
-Plusieurs anciens élèves ont déjà travaillé avec l’encadrant (et ça s’est bien passé). +
- +
-== Stage (potentiellement thèse CIFRE) au SERMA + LaBRI ==  +
- +
-[[https://www.labri.fr/perso/vpenelle/Enseignement/StagesOffres/sujet_stage-M2-Cesti.pdf|Sujet ici]] +
- +
-Titre : Analyse automatisée de binaires appliquée à la recherche de vulnérabilités matérielles. +
- +
-Domaine : vérification. +
- +
-Le SERMA est situé à Pessac et le stage sera co-encadré par des chercheurs du LaBRI (Antoine Rollet et Grégoire Sutre). +
- +
- +
- +
- +
-=== Entreprises === +
- +
-== Stages chez Thalès dans le pôle intelligence artificielle == +
- +
-À Toulouse :  +
- +
-[[https://jobs.thalesgroup.com/job/toulouse/ingenieur-e-interpretation-et-performance-des-raisonnements-ontologie-stage-h-f/1766/18072237| Interprétation et performance des raisonnements (ontologie))]] +
- +
-[[https://jobs.thalesgroup.com/job/toulouse/ingenieur-e-en-traitement-de-donnees-terrain-a-l-aide-de-deep-learning-stage-h-f/1766/18089310|Traitement de données terrain à l’aide de deep learning]] +
- +
-À Bordeaux : +
- +
-[[https://jobs.thalesgroup.com/job/bordeaux/ingenieur-e-digital-twin-stage-h-f/1766/18072240| génération de métriques d'interaction pilote-cockpit-environnement]] +
- +
-== Modélisation par des graphes d’enchevêtrement de longues molécules, à Michelin ==  +
- +
-Nous proposons un stage de master M2 ou dernière année école d'ingénieurs en informatique ou math/info. +
-Ce stage a pour objectif final de modéliser de manière fine la dynamique de l'évolution d'enchevêtrements de longues molécules. +
-Chaque configuration ayant préalablement été représentée sous forme de graphe, il s'agit maintenant de suivre les +
-caractéristiques de ces graphes au cours du temps. +
- +
-La personne recrutée devra idéalement avoir de bonnes connaissances en théorie et algorithmes de graphes, +
-en complexité algorithmique et devra avoir un intérêt pour la compréhension des phénomènes physiques et +
-leur modélisation. Des connaissances préalables en chimie seraient un plus mais ne sont pas strictement indispensables. +
- +
-Lieu du stage : région de Clermont-Ferrand (entreprise Michelin et université Clermont-Auvergne). [[https://www.labri.fr/perso/vpenelle/Enseignement/StagesOffres/Stage_enchevetrement-2.pdf|Le sujet est ici]]. +
- +
-Pour déposer votre candidature, merci de passer obligatoirement par le site : +
- +
-https://recrutement.michelin.fr/fr/stage-michelin +
- +
-== Vérification de systèmes autonomes. == +
- +
-Bonjour,  +
- +
-Je me permets de vous contacter afin de vous faire part d'une offre de stage sur la vérification formelle d'un sous système de nos véhicules autonomes.  +
- +
-Le stage se déroulera au sein de mon équipe dans les locaux de Easymile Toulouse.  +
-Le stage s'inscrit aussi bien dans le cadre d'un master 2 recherche ou Ingénieur 3ème année.  +
- +
-J'ai déjà eu une très bonne expérience avec l'un de vos étudiants en double diplôme recherche/ingénieur, c'est pourquoi j'aimerais pouvoir diffuser largement à vos étudiants (option méthodes formelles).  +
- +
-Je reste à votre disposition pour tout échange sur le sujet.  +
- +
-L'offre de stage est disponible sur : https://www.welcometothejungle.com/en/companies/easymile/jobs/internship-validation-engineer_toulouse +
- +
-En vous remerciant par avance.  +
  
-== Stage R&D programmation logique ==+Suit une liste d’offres reçue pour l’année 2021-2022 (que je tenterai de tenir à jour, et qui concernera sans doute les stages en entreprises, mais pas que).
  
-Anabasis est une jeune entreprise innovante en pleine croissance sur le marché de la modélisation et du développement logiciel. Nous exploitons les technologies de représentation de connaissances pour résoudre le problème de la complexité du cycle de vie d'un système applicatif, de la définition du besoin à la maintenance évolutive. Concrètement, nous utilisons les technologies du web sémantique (OWL/RDF) ainsi qu'une extension du langage de règles SWRL pour représenter, documenter et exécuter les processus métier de nos clients. Nous assurons l'interopérabilité avec les systèmes applicatifs existants au travers de générateurs de code : API, data classes, services WEB.+== Académiques ==
  
 +== Stage au CEA Saclay (avec possibilité de poursuite en thèse) ==
  
-Votre profil+[[https://www.labri.fr/perso/vpenelle/stages-parcours/2022/2022-internships-cyber.pdf | Le sujet. ]] Code-level Cybersecurity & Program Analysis: Vulnerabilities, Verification, Reverse. Stage en vérification formelle, orienté vers l’analyse de binaires. Pour celles et ceux qui aiment la vérif.
  
-Étudiant en Master informatique, vous avez une bonne connaissance de la logique du premier ordre et une appétence marquée pour les systèmes logiques (moteurs d'inférences). Vous connaissez la programmation orientée objet et avez une bonne culture générale en informatique. Des connaissances en programmation logique et/ou fonctionnelle seraient un plus.+== Stage(sau LaBRI avec Loïc Paulevé (poursuite en thèse possible) ==
  
-Mission+[[https://bnediction.github.io/#jobs | Les sujets sont ici.]] Stages sur les réseaux booléens, un modèle de calcul (proche des système d’additions de vecteurs mais avec des booléens) qui est utilisée en modélisation de systèmes biologiques.
  
-Vous interviendrez dans le cadre d'une étude comparative des différentes approches, algorithmes et moteurs existants pour le requêtage de données en lien avec une ontologie. +== Stage (puis thèse) à Reykjavik en théorie des graphes/algo distribuée == 
-Les grandes lignes de cette étude sont les suivantes : +
-1 - État de l'art des approches et algorithmes +
-2 - Identifier les moteurs existants/pertinents +
-3 - Identifier des scénarios de tests pertinents +
-4 - Identifier/réaliser des jeux de tests +
-5 - Mettre en place/automatiser l'exécution des jeux de tests +
-6 - Comparer/analyser les résultats +
-7 - Rapport final+
  
-Vous serez amené à intervenir à différentes étapes de cette étude en fonction de son avancée, de vos goûts et compétences.+Je me permets de relayer cette proposition de doctorat a l'université de Reykjaviksous la direction de Magnús Halldórsson, a transférer a vos étudiants. Avec une précision : les étudiants devant faire un stage de M2 avant de commencer un doctorat sont encouragés a postuler, il y a possibilité de rémunérer un stage de M2 a un niveau de salaire 80~100% équivalent au niveau annoncé pour le doctorat (qui est d'environ 2500€ brut / 1950€ net par mois. A noter que la vie est plus chère ici).
  
- Modalités+Le profil recherché est étudiant.e ou jeune diplômé.e d'un M2 orienté recherche, avec des connaissances en algorithmes randomisés. Un bagage en théorie des graphes et/ou algorithmes distribués est un plus mais n'est pas nécessaire. Candidatures a envoyer a cette adresse (alexandren@ru.is). Ne pas hésiter a me contacter pour poser des questions, discuter informellement, se renseigner et savoir si le poste a été pourvu.
  
-À pourvoir dès que possible. +== Eugène Asarin à l’IRIF (automates temporisés) ==
-800 € nets/mois. +
-Travail basé à Paris, combinable avec du télétravail suivant modalités pratiques à définir.+
  
 +[[https://www.irif.fr/~asarin/#Master | Page personnelle d’Eugène Asarin]]. Il propose des stages sur les automates temporisés et les systèmes cyber-physique). Assez vérif (mais coté automates).
  
-Contact+== Julien Baste et Lætitia Jourdan (Complexité paramétrée) ==
  
-Clément Sipieter+[[https://www.labri.fr/perso/vpenelle/Sujet_master_pc_moo.pdf | Sujet du stage]]. Ce stage se veut une introduction à la complexité paramétréeson adaptation à l’optimisation de plusieurs paramètres et son application au problème de vertex cover (via la conception d’un algorithme adapté). 
-Téléphone : +33 6 75 17 76 31 +Possibilité d’obtenir un financement de thèse en poursuite du stage
-sipieter@anabasis-assets.com +[[https://www.iut-info.univ-lille.fr/~julien.baste/ | Page personnelle de Julien Baste]]
-www.anabasis-assets.com+
  
  
 +[[if-stages-archives|Archives des années précédentes]]
if-stages.1608044532.txt.gz · Dernière modification : 2020/12/15 15:02 de vpenelle