Abstract
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.
Date
Jul 12, 2021
Event
SYFI Workshop 2021
Location
Banyuls
Baptiste Pollien
PhD Student in Formal Methods
My research interests focus on formal methods applied for UAV Autopilot.