Formal Verification of an UAV autopilot: Static analysis and Verified Code Generation. (Vérification formelle du fonctionnement d'un autopilote: Analyse statique et Génération de code vérifiée)

Baptiste Pollien. Formal Verification of an UAV autopilot: Static analysis and Verified Code Generation. (Vérification formelle du fonctionnement d'un autopilote: Analyse statique et Génération de code vérifiée). PhD thesis, Institut supérieur de l'aéronautique et de l'espace, Toulouse, France, 2023. [doi]