En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)
Portail > Offres > Offre UMR5104-DAVMON0-001 - Post-doctorant ou post-doctorante en formalisation du langage Rust et compilation formellement vérifiée (H/F)

Post-doctorant ou post-doctorante en formalisation du langage Rust et compilation formellement vérifiée (H/F)

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

Date Limite Candidature : mardi 17 décembre 2024 23:59:00 heure de Paris

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler

Informations générales

Intitulé de l'offre : Post-doctorant ou post-doctorante en formalisation du langage Rust et compilation formellement vérifiée (H/F)
Référence : UMR5104-DAVMON0-001
Nombre de Postes : 1
Lieu de travail : ST MARTIN D HERES
Date de publication : mardi 26 novembre 2024
Type de contrat : Chercheur en contrat CDD
Durée du contrat : 12 mois
Date d'embauche prévue : 1 février 2025
Quotité de travail : Complet
Rémunération : à partir de 2991€/mois brut, suivant expérience
Niveau d'études souhaité : Doctorat
Expérience souhaitée : Indifférent
Section(s) CN : 6 - Sciences de l'information : fondements de l'informatique, calculs, algorithmes, représentations, exploitations

Missions

Le post-doctorant ou la post-doctorante devra formaliser des aspects du langage Rust à l'aide d'un assistant de preuve (a priori Coq), dans un but d'étude préliminaire de la compilation formellement vérifiée de ce langage.

Activités

- Formalisation d'aspects de Rust
- Preuve formelle
- Conception et implémentation d'algorithmes (typage etc.)
- Rédaction et soumission d'articles scientifiques

Compétences

- familiarité avec Rust
- habitude de la preuve formelle, notamment avec Coq
- compétences usuelles en algorithmique, programmation, gestion de projet, systèmes de compilation
- rédaction et soumission d'articles scientifiques

Contexte de travail

équipe de vérification et preuves formelles du laboratoire Verimag, qui développe notamment le logiciel Chamois

Contraintes et risques

n/a

Informations complémentaires

NA