About me
I'm a PhD candidate in computer science in the SyCoMoRES team at Inria Lille, coadvised by Raphaël Monat, Aymeric Fromherz, and Patrick Baillot.
I'm interested in improving the quality of software systems using automated formal methods. As part of the AVoCat research project, my work focuses the automatic verification of programs implementing legal texts, and particularly those written in Catala, a domain-specific programming language for computational law. I aim to design analyses that are tailored to programs encoding the law, and that lawyers may find useful and usable.
Contact
Email: firstname.lastname@inria.fr
Research
Publications
Hopefully coming soon :)Preprints
-
CUTECat: Concolic Execution for Computational Law
Pierre Goutagny, Aymeric Fromherz, Raphaël Monat.
Talks
- Upcoming: CUTECat: Concolic Execution for Computational Law
Workshops
-
CUTECat: Generating Testcases for Fiscal Laws through Concolic Execution
Pierre Goutagny, Aymeric Fromherz, Raphaël Monat. Programming Languages and the Law (ProLaLa) workshop, 2024.
Previous research experience
As a computer science student at École normale supérieure de Lyon from 2020 to 2024, I have completed research internships where I have experimented with program analysis, and with mechanized verification in the Rocq proof assistant, with potential applications to compilers, operating systems code, research tooling, and more recently data science and computational law.
-
Static Analyses for Dataframes.
Supervised by Caterina Urban. École normale supérieure - PSL, Paris, France. 2024.
-
CUTECat: A Concolic Unit Testing Engine for the Catala Language.
Supervised by Raphaël Monat and Aymeric Fromherz. Inria Lille, France. 2023-24.
-
Kleene Algebras with Hypotheses: Modular Formalisation.
Supervised by Damien Pous. École normale supérieure de Lyon, France. 2023.
-
Towards the Verification of Circular Data Structures in RefinedC.
Supervised by Freek Wiedijk and Robbert Krebbers. Radboud University, Nijmegen, The Netherlands. 2022.
-
Optimization in Certified Compilation.
Supervised by Sylvain Boulmé and David Monniaux. Verimag, Grenoble, France. 2021.
This work's Rocq code is published as part of the Chamois project.