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