Le but de mes recherches est d’améliorer la qualité des logiciels. J’utilise pour cela le domaine des méthodes formelles, afin de définir précisément le comportement des programmes. Cela permet de raisonner rigoureusement sur ces comportements (pour déceler par exemple des états dangereux). Je présenterai dans cet exposé mes recherches sur deux systèmes réalistes. Le premier système est le langage de programmation Python, qui est très populaire. C’est en particulier le langage le plus utilisé sur GitHub. Je présenterai en particulier une analyse multilangage, permettant de détecter des bogues dans les programmes utilisant à la fois Python et C. Cette analyse répond à un besoin réel : les programmes sont souvent écrits avec plusieurs langages, mais ce problème n’a été que peu étudié précédemment. Je détaillerai les travaux d’implémentations dans la plateforme d’analyse statique Mopsa. Ces travaux ont été effectués durant ma thèse, avec Antoine Miné et Abdelraouf Ouadjaout (LIP6, Sorbonne Université).
Le second système est le code de calcul de l’impôt sur le revenu des particuliers. Ce système est critique : il concerne 38 millions de foyers fiscaux français, et rapporte 30% des recettes de l’État chaque année. Ce travail de recherche a été effectué en collaboration avec Denis Merigoux (Prosecco, Inria Paris). J’exposerai comment nos recherches ont permis de rendre le calcul de l’impôt sur le revenu publiquement reproductible, ainsi que le transfert de nos travaux auprès de l’administration fiscale.