Interprétation abstraite

Vérification d'une bibliothèque mathématique d'un autopilote avec Frama-C
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.