I am a PhD student at ISAE-SUPAERO, in Toulouse. My thesis deals with formal methods applied on UAV autopilot, especially Paparazzi autopilot developed at ENAC. I am currently working on the verification of the Paparazzi flight plan generator using Coq. I previously worked on the verification of a mathematical library of Paparazzi using Frama-C with EVA and WP plugins. I focused on the verification of the absence of runtime errors (overflows, divisions by 0…) but I also verified some functional properties.
PhD in Formal Methods, Present
ISAE-SUPAERO - Toulouse, FRANCE
Master’s Degree in Engineering, 2020 - 2017
ENSIMAG - Grenoble, FRANCE
Preparation for entry to engineering schools, 2017 - 2015
Univ. Grenoble Alpes - Grenoble, FRANCE
Commissioned by the NSIGMA Junior entreprise of ENSIMAG.