Master Informatique - Université de Bordeaux

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).

Pour les stages dans un laboratoire de recherche en France ou à l’étranger, la première étape est d’identifier le domaine général dans lequel vous souhaitez travailler et le (ou les) pays vous intéressant.

Une fois cela fait, vous pouvez envisager de contacter des chercheurs travaillant dans le domaine qui vous intéresse pour leur demander de l’aide et pourquoi pas un stage. Vos enseignants peuvent vous aider à trouver des spécialistes de ce qui vous intéressent et vous aider à les contacter.

Pour les stages au LaBRI, une page moodle recense les stages proposés en son sein, mais rien ne vous empêche de contacter un membre du laboratoire et de concevoir un sujet de stage avec lui.

Dans tous les cas, réfléchissez (éventuellement avec votre encadrant potentiel) si vous souhaitez poursuivre en thèse ou pas : les stages ne sont pas nécessairement les mêmes si l’on souhaite poursuivre ou pas, la question du financement peut être compliquée, et il est toujours délicat que l’encadrant et le stagiaire ne soient pas d’accord sur la poursuite ou non en thèse.

Pour les stages en entreprises, nous recevons régulièrement des offres par des contacts habituels qui seront postés sur la présente page s’ils concernent les domaines au cœur de IF. Vos enseignants ont bien évidemment moins de liens et de connaissance du monde industriel que du monde académique, donc même si nous vous aiderons au mieux, nous aurons moins de pointeurs.

Il ne faut pas hésiter à consulter des offres de stages postées par des entreprises travaillant dans des domaines vous intéressant, ou à les contacter directement (si vous avez un bon pointeur).

Suit une liste d’entreprises proposant régulièrement des stages qui peuvent vous intéresser :

• à l’ONERA
• à l’ANSSI
• au CEA
• à l’ANSYS
• chez THALES
• chez Airbus
• chez Systerel
• chez MBDA
• chez Siemens
• chez Mitsubishi R&D
• chez CLEARSY (suivre une auto formation à la méthode B avant de postuler)

En complément, des moteurs de recherche de stages tels que jooble ou indeed peuvent valoir d’être consultés.

Dans tous les cas, n’hésitez pas à parler des offres que vous avez vues avec vos enseignants (on ne garantie pas d’être pertinents, mais on essaiera).

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).

Vous pouvez trouver 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.

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

Sujet ici

Titre : Testing Deep Neural Network

Domaine : vérification et apprentissage.

Encadrant : Antoine Rollet.

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.

Sujet détaillé

Mots-clés: synthèse de programme, apprentissage, test

Financement non acquis.

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.

Sujet Détaillé

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.

Sujet Détaillé

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

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

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

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é).

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).

À Toulouse :

Interprétation et performance des raisonnements (ontologie))

Traitement de données terrain à l’aide de deep learning

À Bordeaux :

génération de métriques d'interaction pilote-cockpit-environnement

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). Le sujet est ici.

Pour déposer votre candidature, merci de passer obligatoirement par le site :

https://recrutement.michelin.fr/fr/stage-michelin

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.

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.

Votre profil

É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.

Mission

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. 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.

Modalités

À pourvoir dès que possible. 800 € nets/mois. Travail basé à Paris, combinable avec du télétravail suivant modalités pratiques à définir.

Contact

Clément Sipieter, Téléphone : +33 6 75 17 76 31 sipieter@anabasis-assets.com www.anabasis-assets.com