En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)
Portail > Offres > Offre UMR9021-PATBOU-006 - Post-doctorat (H/F) : Analyse et vérification des systèmes d'addition de vecteurs d'entiers et de leurs extensions.

Post-doctorat (H/F) : Analyse et vérification des systèmes d'addition de vecteurs d'entiers et de leurs extensions.

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

Date Limite Candidature : mercredi 13 juillet 2022

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 !

Informations générales

Référence : UMR9021-PATBOU-006
Lieu de travail : GIF SUR YVETTE
Date de publication : mercredi 1 juin 2022
Type de contrat : CDD Scientifique
Durée du contrat : 16 mois
Date d'embauche prévue : 1 septembre 2022
Quotité de travail : Temps complet
Rémunération : Entre 2 663,79€ brut mensuel et 3 783,24€ brut mensuel selon expérience
Niveau d'études souhaité : Doctorat
Expérience souhaitée : 1 à 4 années

Missions

Dans le cadre du projet ANR BRAVAS, nous nous intéressons à l'analyse et la vérification des systèmes d'addition de vecteurs d'entiers et de leurs extensions.

Activités

- Analyse et vérification des systèmes d'addition de vecteurs.
- Analyse et vérification des machines à compteurs et de leurs extensions.
- Algorithmique des propriétés d'accessibilité.

Compétences

La personne recrutée devra posséder des compétences en :
- Logique, automates et vérification formelle
- Algorithmique de la vérification
- Modèles concurrents

Contexte de travail

Le/la post-doctorant recruté travaillera au sein du laboratoire LMF. Le Laboratoire Méthodes Formelles (LMF) est un laboratoire d'informatique spécialisé dans le développement de méthodes formelles. Il a trois tutelles principales (CNRS, Université Paris-Saclay, ENS Paris-Saclay) et deux partenaires (Inria, CentraleSupélec). Son ambition est d'éclairer le « monde numérique » grâce à la logique mathématique en utilisant les méthodes formelles comme outil d'analyse, de modélisation et de raisonnement pour les programmes informatiques, les protocoles de sécurité, etc. Il s'appuie sur des paradigmes de calcul des plus classiques aux plus novateurs comme l'informatique quantique. Le LMF est structuré en pôles : son cœur de métier en comporte deux, « Preuves et langages » et « Modèles » ; le troisième, « Interactions », est une ouverture à d'autres domaines tels que l'intelligence artificielle ou la biologie. Il est l'un des laboratoires leaders mondiaux dans son domaine.

Le LMF est localisé sur le plateau du Moulon (91), dans les locaux de l'ENS Paris-Saclay et dans le bâtiment 650 de l'Université Paris-Saclay.
Le laboratoire est composé d'une centaine de membres, dont une cinquantaine de chercheurs (CNRS, Inria) ou d'enseignants-chercheurs (Université Paris-Saclay, ENS Paris-Saclay, CentraleSupélec).
Le post-doctorant recruté travaillera au sein de l'équipe Model checking, dont l'objectif est le développement de modèles, logiques, algorithmes et outils de vérification.

Contraintes et risques

travail sur écran

On en parle sur Twitter !