Application of formal methods for interferences management H/F

Job description: Within a multidisciplinary technological research team of experts in SW/HW co-design tools by applying formal methods, you will be involved in a national research project aiming at developing an environment to identify, analyze and reduce the interferences generated by the concurrent execution of applications on a heterogeneous commercial-off-the-shelf (COTS) multi-core hardware platform. Your main missions will be : To propose and develop a formal modeling strategy for the temporal behavior of the hardware platform's microarchitecture and memory hierarchy based on microbenchmarking results of the platform. The microbenchmarking results are produced by a project partner. This modeling will be used to identify interferences and the impact of temporal anomalies on memory accesses, especially their temporal predictability. To propose and develop an approach to make the execution of applications more predictable by reducing the interferences identified in point 1. via the definition of specific rules at the level of their execution model but also at the level of their programming model to guide code synthesis. The whole will be enhanced by the integration of such an approach within a compilation environment chosen by the project partners. You are also expected to : Communicate about the work to the project partners, but also work directly with the French and German partners of the project; Participate in the scientific dissemination of the team's research results (contributions to publications in international conferences) and in the development of our innovations (writing of patents). To carry out your mission, you will benefit from a first class environment at CEA LIST with access to a large number of reference tools and a strong experience in the application of formal methods to the verification of properties such as temporal anomalies.

Your profile: 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.

Languages: English Fluent,French Fluent