Baptiste Pollien

Registered user since Thu 2 Mar 2023

Name:Baptiste Pollien
Bio:

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.

Country:France
Affiliation:ISAE-SUPAERO
Research interests:Formal Methods, Coq, Frama-C, Critical Systems

Contributions