Combinaison de sur et sous-approximations pour lapos;analyse de programmes bas-niveau

Description de l'offre : Parce que lapos;analyse de programme est un problème indécidable, les analyses statiques se divisent en 2 catégories: - Les analyses sound, qui calculent une surapproximation de tous les comportements du programme, et permettent de vérifier lapos;absence dapos;erreur. - Les analyses complete, qui calculent une sous-approximation des comportements possibles du programme, et permettent de trouver des erreurs. Le but de la thèse est dapos;étudier cette combinaison de ces techniques pour lapos;analyse statique de programmes bas-niveau, en particulier des exécutables binaires, en ciblant notamment les analyses de la mémoires et du flot de contrôle, qui sont les informations capitales pour comprendre les comportements possibles dapos;un binaire. [POPLapos;23]: SSA Translation is an Abstract Interpretation, M. Lemerre (Distinguished paper award) [VMCAIapos;22]: Lightweight Shape Analysis Based on Physical Types, O. Nicole, M. Lemerre, X. Rival [RTASapos;21]: No Crash, No Exploit: Automated Verification of Embedded Kernels, O. Nicole, M. Lemerre, S. Bardin, X. Rival (best paper award) [LPARapos;18] Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing B. Farinier, S. Bardin, R. David, M. Lemerre

Profil du candidat : Master informatique ou Ecole dapos;ingenieu. Bagage en vérification/analyse statique,programmation en OCaml, connaissance du C ou assembleur, sont des avantages.