Doctorant en Langages Orientés Interaction et Vérification

Ecole Nationale de l'Aviation Civile; France; Sur place; EUR 40 000 - 60 000; Plein temps

Résumé du poste

Un institut de recherche en aéronautique recherche un candidat pour formaliser le langage Smala et sa sémantique dans le cadre d'un projet de recherche. Le candidat sera chargé de développer la compilation vers le langage C et de vérifier la cohérence du processus. Un master en informatique et une expérience avec les méthodes formelles, le prouveur Rocq, et la programmation OCaml sont exigés. Une connaissance des systèmes de gestion du trafic aérien est un plus.

Qualifications

• Le candidat doit être titulaire d'un master (ou équivalent) en informatique.
• Familiarité avec les méthodes formelles, le prouveur Rocq, OCaml, et la compilation requise.
• Connaissance de la programmation IHM et/ou des systèmes de gestion du trafic aérien appréciée.

Responsabilités

• Formaliser le langage Smala et sa sémantique.
• Implémenter la compilation vers le langage de bas niveau C.
• Développer une preuve mécanisée de la compilation.

Connaissances

Méthodes formelles

Proveur Rocq

Programmation OCaml

Compilation

Formation

Master en informatique ou équivalent

Description du poste

Un institut de recherche en aéronautique recherche un candidat pour formaliser le langage Smala et sa sémantique dans le cadre d'un projet de recherche. Le candidat sera chargé de développer la compilation vers le langage C et de vérifier la cohérence du processus. Un master en informatique et une expérience avec les méthodes formelles, le prouveur Rocq, et la programmation OCaml sont exigés. Une connaissance des systèmes de gestion du trafic aérien est un plus.