Le CNES développe des équipements qui contribuent à la protection des personnes, des biens, de la santé publique et de l’environnement pendant les lancements spatiaux. Certains de ces équipements sont développés au plus haut niveau de criticité, le DAL A de la norme DO-178C, et implémentent des algorithmes, et en particulier des algorithmes géométriques, qui doivent être robustes et efficaces.
Dans ce cadre, nous souhaitons:
* Faire une modélisation formelle, dans l’assistant de preuve Coq/Rocq, d’un équipement en développement, afin de repérer ses erreurs de conception de manière exhaustive. La modélisation formelle sera également exécutable, permettant de l’utiliser comme un simulateur de l’équipement; et/ou
* Faire une étude comparative entre des algorithmes de détection de l’appartenance d’un point dans un polygone (le problème point-in-polygon) qui sont susceptible d’être utilisés. L’étudiant poursuivant un cursus théorique pourrait aussi travailler sur la preuve formelle de la correction de ces algorithmes en utilisant, par exemple, l’outil Gappa; et/ou
* Travailler sur une interface homme-machine afin d’obtenir le simulateur à partir du modèle exécutable, ceci exigeant une connaissance des langages de programmation C ou C++.
Le stage pourrait débuter au printemps 2026.
En cliquant sur "JE DÉPOSE MON CV", vous acceptez nos CGU et déclarez avoir pris connaissance de la politique de protection des données du site jobijoba.com.