Combinaison de sur et sous-approximations pour l'analyse de programmes bas-niveau

Parce que l'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 l'absence d'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 d'étudier cette combinaison de ces techniques pour l'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 d'un binaire. [POPL'23]: SSA Translation is an Abstract Interpretation, M. Lemerre (Distinguished paper award) [VMCAI'22]: Lightweight Shape Analysis Based on Physical Types, O. Nicole, M. Lemerre, X. Rival [RTAS'21]: No Crash, No Exploit: Automated Verification of Embedded Kernels, O. Nicole, M. Lemerre, S. Bardin, X. Rival (best paper award) [LPAR'18] Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing B. Farinier, S. Bardin, R. David, M. Lemerre