Verifying the Mathematical Library of a UAV Autopilot with Frama-C


During the development of a critical system, such as a drone autopilot, it is essential to ensure that the program is safe, for example using formal methods. To facilitate verification, we generally restrict ourselves to an abstraction of the system or a subset. This article presents the verification of a mathematical library of the Paparazzi autopilot, using the Frama-C tool, in order to guarantee the absence of runtime errors and certain functional properties.

Jul 12, 2021
SYFI Workshop 2021
Baptiste Pollien
Baptiste Pollien
PhD Student in Formal Methods

My research interests focus on formal methods applied for UAV Autopilot.