En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)
Portail > Offres > Offre UMR5668-MARNAR-003 - 2 postes - POST DOCTORANT H/F – LOGIQUE ET VÉRIFICATION - LYON

2 postes - POST DOCTORANT H/F – LOGIQUE ET VÉRIFICATION - LYON

Cette offre est disponible dans les langues suivantes :
Français - Anglais

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler. Les informations de votre profil complètent celles associées à chaque candidature. Afin d’augmenter votre visibilité sur notre Portail Emploi et ainsi permettre aux recruteurs de consulter votre profil candidat, vous avez la possibilité de déposer votre CV dans notre CVThèque en un clic !

Faites connaître cette offre !

Informations générales

Référence : UMR5668-MARNAR-003
Lieu de travail : LYON 07
Date de publication : mardi 17 septembre 2019
Type de contrat : CDD Scientifique
Durée du contrat : 12 mois
Date d'embauche prévue : 1 novembre 2019
Quotité de travail : Temps complet
Rémunération : Entre 2617 et 3729€ bruts mensuels selon expérience
Niveau d'études souhaité : Doctorat
Expérience souhaitée : 1 à 4 années

Missions

Le candidat retenu sera engagé pour un post-doctorat de 12 mois afin de mener des recherches originales dans
le cadre du projet CoVeCe (Coinduction for Verification and Certification). La recherche sera effectuée au LIP (ENS - Lyon, France) au sein de l'équipe "PLUME" sous la supervision de Damien Pous (CNRS).

Activités

L'objectif est d'étudier des systèmes de preuve et des algorithmes pour certaines extensions des algèbres de Kleene, puis d'implémenter les outils correspondants au sein de l'assistant de preuve Coq.
Selon le candidat, les travaux pourront porter plus sur les aspects logiques du problème, plus sur ses aspects algorithmiques, ou plus sur l'aspect formalisation en Coq.

Compétences

Les candidats doivent avoir terminé (ou être sur le point de terminer) un doctorat en informatique théorique. Idéalement, le candidat aura déjà une bonne connaissance de plusieurs des sujets suivants: automates, algèbres de Kleene, systèmes de preuves cycliques, graphes de largeur d'arbre bornée, coinduction, assistants de preuves.

Contexte de travail

La recherche s'effectuera au laboratoire LIP (ENS - Lyon, France) au sein de l'équipe "PLUME" sous la supervision de Damien Pous (CNRS), dans le cadre de son ERC starting grant 'CoVeCe'.
L'équipe PLUME (LIP, ENS-Lyon) s'intéresse aux fondements mathématiques pour la correction des programmes: systèmes de types, logique, logique linéaire, algèbres de processus, vérification de modèles, assistants de preuve, complexité implicite.
Le project CoVeCe s'intéresse aux applications de la coinduction et d'algorithmes d'automates pour faciliter des tâches de vérification et de certification (i.e., en Coq).

Contraintes et risques

Le laboratoire LIP n'est pas un laboratoire expérimental et ne comporte pas de contraintes et risques particuliers.

On en parle sur Twitter !