Postdoc application des méthodes formelles pour la gestion des interférences H/F

Description de l'offre : Au sein d'une équipe de recherche technologique multidisciplinaire composée d'experts en co-conception matériel/logiciel utilisant des méthodes formelles, vous participerez à un projet de recherche national visant à développer un environnement permettant d'identifier, d'analyser et de réduire les interférences générées par l'exécution concurrente d'applications sur une plateforme matérielle hétérogène multi-cœurs de type COTS (Commercial-Off-The-Shelf). Vos principales missions seront : Proposer et développer une stratégie de modélisation formelle pour le comportement temporel de la microarchitecture de la plateforme matérielle et de la hiérarchie mémoire, basée sur les résultats de microbenchmarking de la plateforme. Les résultats de microbenchmarking sont produits par un partenaire du projet. Cette modélisation sera utilisée pour identifier les interférences et l'impact des anomalies temporelles sur les accès mémoire, en particulier leur prévisibilité temporelle. Proposer et développer une approche pour rendre l'exécution des applications plus prévisible en réduisant les interférences identifiées au point 1, via la définition de règles spécifiques au niveau de leur modèle d'exécution mais aussi au niveau de leur modèle de programmation pour guider la synthèse du code. L'ensemble sera amélioré par l'intégration de cette approche dans un environnement de compilation choisi par les partenaires du projet. Vous devrez également : Communiquer sur le travail avec les partenaires du projet, et travailler directement avec les partenaires français et allemands du projet; Participer à la diffusion scientifique des résultats de recherche de l'équipe (contributions à des publications dans des conférences internationales) et au développement de nos innovations (rédaction de brevets). Pour mener à bien votre mission, vous bénéficierez d'un environnement de premier ordre au CEA LIST avec accès à un grand nombre d'outils de référence et une forte expérience dans l'application des méthodes formelles à la vérification de propriétés telles que les anomalies temporelles.

Profil du candidat : Vous êtes titulaire d'un doctorat dans le domaine de l'électronique ou des systèmes embarqués. Vous avez une expérience significative en architecture et/ou compilation ainsi que dans l'utilisation des méthodes formelles. Vous avez également une première expérience dans la conception et la vérification/validation des applications temps réel sur des architectures multicœurs. Vous aimez travailler dans un environnement de recherche appliquée à la pointe de la technologie et proposer des innovations dans divers domaines d'application. Vous avez acquis les compétences techniques suivantes : Architecture et programmation des ordinateurs : connaissance des architectures multi/many-core et de leur utilisation dans un contexte d'exécution des applications temps réel, analyse du temps d'exécution dans le pire des cas, formalisation des ensembles d'instructions d'architecture (tels que SAIL), connaissance des langages de description d'architecture matérielle (HDL) Méthodes formelles : langage de spécification formelle, environnement de model-checking, solveurs SMT, etc. Compilation : connaissance des environnements de conception pour les systèmes temps réel (par exemple, programmation synchrone), chaînes de compilation (LLVM / GCC) Une expérience en termes d'interaction avec des partenaires dans des projets collaboratifs et/ou industriels ainsi que des publications scientifiques est également attendue. Qualités personnelles souhaitées : Capacité à travailler en équipe, tout en montrant une bonne autonomie au quotidien ; Curiosité scientifique, goût pour les défis techniques ; Capacité à comprendre et résoudre des problèmes complexes ; Capacité à prendre du recul et avoir une vision transversale ; Méthodes de travail rigoureuses et esprit de synthèse.

Langues : Anglais Courant,Français Courant