Transformations source à source prouvées pour l'architecture Arm

Ce projet de thèse s'inscrit dans le cadre de la compilation source-à-source des programmes, qui permet des optimisations de haut niveau, portables sur différentes architectures. Il cible des programmes et des librairies, développées pour architecture x86, que le partenaire industriel de cette thèse, ARM, souhaite migrer vers son architecture de manière efficace et sûre. Il s'agira notamment de prendre en compte les instructions vectorielles et d'exploiter les fonctions intrinsèques, ainsi que d'utiliser des outils permettant de garantir formellement que les traductions préservent le comportement sémantique du code. École doctorale : ISMME - Ingénierie des Systèmes, Matériaux, Mécanique, Énergétique Direction : Olivier HERMANT Financement : CIFRE ANRT