Méthodes déductives

This french article presents the verification of a mathematical library of the autopilot Paparazzi, using the Frama-C tool, in order to guarantee the absence of runtime error and some functional properties.