Ci-dessous, les différences entre deux révisions de la page.
Les deux révisions précédentesRévision précédenteProchaine révision | Révision précédente | ||
if-stages [2020/12/15 15:02] – vpenelle | if-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), | + | 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), |
+ | |||
+ | 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:// | ||
+ | * 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 pourrez trouver plus de détail sur la procédure complète [[https:// | ||
=== Stages académiques === | === Stages académiques === | ||
Ligne 37: | Ligne 54: | ||
- | === Offres | + | === Offres |
- | + | ||
- | 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, | + | |
- | + | ||
- | === Académiques === | + | |
- | + | ||
- | == Équipe MF == | + | |
- | + | ||
- | Vous pouvez trouver [[https:// | + | |
- | + | ||
- | == Stage puis thèse à Lyon (traces d’exécutions et inférences de schémas de compilations polyédriques) == | + | |
- | + | ||
- | Dans le cadre de l' | + | |
- | à l’Ecole Normale Supérieure de Lyon. | + | |
- | + | ||
- | L’objectif principal de ce projet est d' | + | |
- | + | ||
- | Une description détaillée, | + | |
- | + | ||
- | http:// | + | |
- | + | ||
- | N' | + | |
- | + | ||
- | Christophe Alias | + | |
- | Chargé de recherche HDR | + | |
- | Inria/ENS de Lyon | + | |
- | http:// | + | |
- | + | ||
- | == Stage au LaBRI == | + | |
- | + | ||
- | [[https:// | + | |
- | + | ||
- | Titre : Testing Deep Neural Network | + | |
- | + | ||
- | Domaine : | + | |
- | + | ||
- | 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, | + | |
- | + | ||
- | [[https:// | + | |
- | + | ||
- | + | ||
- | Mots-clés: synthèse de programme, apprentissage, | + | |
- | + | ||
- | Financement non acquis. | + | |
- | + | ||
- | == Stage au Limos (Clermont-Ferrand) == | + | |
- | + | ||
- | Titre: | + | |
- | + | ||
- | Encadrants: | + | |
- | + | ||
- | Résumé: | + | |
- | + | ||
- | Mots clés: | + | |
- | + | ||
- | Poursuite en thèse possible. | + | |
- | + | ||
- | [[https:// | + | |
- | + | ||
- | + | ||
- | + | ||
- | == Stage à Inria Bordeaux == | + | |
- | + | ||
- | Title: Design of an Interactive Demo on Multi-task Deep Reinforcement Learning using Procedurally Generated Environments | + | |
- | + | ||
- | Encadrants : | + | |
- | + | ||
- | Domaine : | + | |
- | + | ||
- | Stage à forte componsante ingéniérie et notamment développement web. | + | |
- | + | ||
- | [[https:// | + | |
- | + | ||
- | == 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 | + | |
- | Cette logique contient deux modalités [E] et [C] indexées par des | + | |
- | agents: une formule [E] _i A est interprété comme «l' | + | |
- | en sorte que A», tandis que une formules [C] _i A est interprété comme | + | |
- | «l' | + | |
- | 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. | + | |
- | 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' | + | |
- | si une formule de logique de Elgesem est valide ou pas | + | |
- | en produisant une preuve ou un contre-modèle. | + | |
- | 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, | + | |
- | Mathématiques, | + | |
- | la logique. | + | |
- | Des connaissances de base de la logique, et des logiques modales en | + | |
- | particulier, | + | |
- | 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' | + | |
- | + | ||
- | 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' | + | |
- | Nicola Olivetti, LIS, Univ. d' | + | |
- | + | ||
- | == Thèse à Londres == | + | |
- | + | ||
- | Proposition de doctorat à Londres. Contactez-les éventuellement pour un stage si vous êtes intéressés. | + | |
- | + | ||
- | Contact: | + | |
- | + | ||
- | Mots clé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 | + | |
- | + | ||
- | + | ||
- | 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. | + | |
- | + | ||
- | 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; | + | |
- | 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, | + | |
- | + | ||
- | 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' | + | |
- | associated with ECOOP and OOPSLA, on 16th and 17th November, and at Facebook' | + | |
- | + | ||
- | [2] Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic, Azalea Raad (Imperial), Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O' | + | |
- | + | ||
- | [3] A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications, | + | |
- | + | ||
- | [4] A Perspective on Specifying and Verifying Concurrent Modules, Thomas Dinsdale-Young, | + | |
- | + | ||
- | [5] Data Consistency in Transactional Storage Systems: a Centralised Approach, Shale Xiong, Andrea Cerone, Azalea Raad and Philippa Gardner, ECOOP' | + | |
- | + | ||
- | == 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' | + | |
- | + | ||
- | Le projet | + | |
- | Les offres | + | |
- | Le cadre formel --> https:// | + | |
- | + | ||
- | Les laboratoires : | + | |
- | * LIRIS/ | + | |
- | * LIP6/ | + | |
- | * Cedric/ | + | |
- | * DDS/ | + | |
- | + | ||
- | + | ||
- | === Stages Mixtes Entreprise - Recherche === | + | |
- | + | ||
- | == Stage -- avec débouché en thèse potentiel -- à Thalès == | + | |
- | + | ||
- | [[https:// | + | |
- | + | ||
- | 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:// | + | |
- | + | ||
- | 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:// | + | |
- | + | ||
- | [[https:// | + | |
- | + | ||
- | À Bordeaux : | + | |
- | + | ||
- | [[https:// | + | |
- | + | ||
- | == 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' | + | |
- | Ce stage a pour objectif final de modéliser de manière fine la dynamique de l' | + | |
- | 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:// | + | |
- | + | ||
- | Pour déposer votre candidature, | + | |
- | + | ||
- | https:// | + | |
- | + | ||
- | == 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' | + | |
- | + | ||
- | J'ai déjà eu une très bonne expérience avec l'un de vos étudiants en double diplôme recherche/ | + | |
- | + | ||
- | Je reste à votre disposition pour tout échange sur le sujet. | + | |
- | + | ||
- | L' | + | |
- | + | ||
- | 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, |
- | 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, | + | == Académiques == |
+ | == Stage au CEA Saclay (avec possibilité de poursuite en thèse) == | ||
- | Votre profil | + | [[https:// |
- | Étudiant en Master informatique, | + | == Stage(s) au LaBRI avec Loïc Paulevé (poursuite |
- | Mission | + | [[https:// |
- | Vous interviendrez dans le cadre d'une étude comparative des différentes approches, algorithmes et moteurs existants pour le requêtage de données | + | == Stage (puis thèse) à Reykjavik |
- | Les grandes lignes de cette étude sont les suivantes : | + | |
- | 1 - État de l'art des approches et algorithmes | + | |
- | 2 - Identifier les moteurs existants/ | + | |
- | 3 - Identifier des scénarios de tests pertinents | + | |
- | 4 - Identifier/ | + | |
- | 5 - Mettre en place/ | + | |
- | 6 - Comparer/analyser les résultats | + | |
- | 7 - Rapport final | + | |
- | Vous serez amené à intervenir à différentes étapes | + | Je me permets |
- | | + | 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, |
- | À pourvoir dès que possible. | + | == Eugène Asarin |
- | 800 € nets/ | + | |
- | Travail basé à Paris, combinable avec du télétravail suivant modalités pratiques à définir. | + | |
+ | [[https:// | ||
- | Contact | + | == Julien Baste et Lætitia Jourdan (Complexité paramétrée) == |
- | Clément Sipieter, | + | [[https:// |
- | 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/ |
- | www.anabasis-assets.com | + | |
+ | [[if-stages-archives|Archives des années précédentes]] |