Master Informatique - Université de Bordeaux

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

The Department of Informatics, Communication and Systems at the University of Milano-Bicocca invites applications for a PhD position in Algorithms in Pangenome Informatics

The position is funded by the Innovative Training Network (ITN) project “Algorithms for PAngenome Computational Analysis (ALPACA)” of the Horizon 2020 Marie Skłodowska-Curie (MSC) Work Programme.

The salary is competitive and complies with the MSC Work Programme: 3500 euros per month before taxes, consisting of Living and Mobility allowance after compulsory deductions. A conditional Family allowance of 385 euros can be added to the salary.

The candidate will join the team of the BIAS-lab of Professor Paola Bonizzoni and will work on a research project that will be conducted with collaborators from the ALPACA network (https://alpaca-itn.eu/).

The application deadline is Feb 15, 2021.

For more information, see:

https://algolab.eu/grants/phd-position-available/

How to apply

Please submit your application by sending directly by email the application to Professor Paola Bonizzoni (paola.bonizzoni@unimib) cc’ing Professor Gianluca Della Vedova (gianluca.dellavedova@unimib.it).

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