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 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.