The goal of my research is to improve the quality of software. I use for that the field of formal methods, in order to define precisely the behavior of programs. This allows to reason rigorously about these behaviors (to detect dangerous states for example). During the last four years, I have studied two realistic systems, with different collaborators.
The first system is the very popular Python programming language. In particular, it is the second most used language (after JavaScript) on GitHub. This system is the subject of research done during my thesis with Antoine Miné and Abdelraouf Ouadjaout. I will present a multilanguage analysis, allowing to detect bugs in programs using both Python and C. This analysis answers a real need: programs are often written with several languages, but this problem has been little studied before. I will detail the implementation work in the static analysis platform Mopsa, developed in the framework of an ERC project.
The second system is the personal income tax calculation code. This system is critical: it concerns 38 million French tax households, and brings in 30% of the government’s revenue each year. This research work was done in parallel with my thesis, in collaboration with Denis Merigoux (then a PhD student in Prosecco, Inria Paris). I will explain how our research allowed us to make the income tax calculation publicly reproducible, as well as the transfer of our work to the tax administration.