Dans des travaux récents [RTAS 2021], nous avons démontré l'intérêt d'une analyse statique guidée
par un système de types dépendants avancé pour analyses des programmes systèmes bas-niveau, allant
jusqu'à pouvoir vérifier automatiquement l'absence d'escalade de privilège dans un noyau de système
d'exploitation embarqué comme conséquence de la type-safety du code du noyau. La gestion de la
mémoire est un problème particulièrement ardu lors de l'analyse de programmes systèmes, ou plus largement,
de programmes écrits en C, et l'analyse basée sur les types fournit une solution satisfaisante à
applicabilité large (par exemple, code de gestion de structures de données [VMCAI 2022], runtime de
langage dynamique, code applicatif orienté performance, etc.)

Le but de la thèse est d'étendre le applications qui peuvent être faites de l'utilisation d'une analyse
statique basée sur les types.

[RTAS’21] No Crash, No Exploit: Automated Verification of Embedded Kernels. O. Nicole, M. Lemerre,
S. Bardin, X. Rival (Best paper)
[VMCAI’22] Lightweight Shape Analysis based on Physical Types, O. Nicole, M. Lemerre, X. Rival
[POPL’23] SSA Translation Is an Abstract Interpretation, M. Lemerre (Distinguished paper).