Formal verification of the Paparazzi autopilot

This project is a fork of Paparazzi UAV autopilot repository ( The aim of this project is to verify the pprz_algebra library using Frama-C.

The GitLab project adds ACSL annotations and provides a script to automatically launch Frama-C. Frama-C analyses the code, checks for the absence of RTE (RunTime Errors) and verify some functional properties.

Required software

To run the verification, the following software are required:

  • Frama-C 23.0 (Vanadium)
  • Alt-Ergo 2.4.0
  • CVC4 1.9-prerelease
  • Z3 4.8.6
  • Coq 8.12.2
  • Why3 1.4.0
  • ctags

How to launch the verification process

First, go to the sw/airborne directory:

cd sw/airborne

Update the variable FRAMAC_PREFIX in with the path of the directory containing Frama-C binary. Then, launch the script that starts the analysis:


The WP smoke tests can be enabled with the environment variable SMOKE as follows:

SMOKE=1 ./

Quick description of modified files

  • sw/airborne/ a shell script that automatically launches the verification using Frama-C.
  • sw/airborne/ a Python script used by to read and analyse the results from Frama-C.
  • sw/airborne/math/pprz_algebra_(int|float|double).(h|c): the mathematical library of Paparazzi that has been verified. These files have been annotated with ACSL.
  • sw/airborne/math/pprz_algebra_(int|float|double)_frama_c.h: files containing definition of predicates, lemmas and logical functions used to verify the absence of RTE in the library.
  • sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h: definition of predicates, lemmas and logical functions for the verification of functional properties.
  • sw/airborne/.frama-c/wp/interactive: Coq scripts containing the proof lemmas.
  • sw/airborne/.frama-c/wp/script: WP scripts containing the tactics used to prove some goals.

Verification process

The verification process combines the analysis of the EVA and WP plugins of Frama-C. The EVA plugin requires a program entry point (a main or a function) to start its analysis. The script finds automatically all the names of the functions in the library using ctags. Then, verification is launched for every function FUNCTION with the following parameters:

  • -rte: adds RTE annotations in the code.
  • -no-warn-left-shift-negative: allows left shift for negative values.
  • -eva -lib-entry -main $FUNCTION: launches EVA analysis with $FUNCTION as the entry point. The initial state is determined by the preconditions specified in the contract of the function.
  • -wp-fct $FUNCTION: launches the WP verification with the following options:
    • -wp-cache update: enables and uses cache.
    • -wp-model real+Cast+ref: enables the real model to represent the arithmetic on floating-point numbers. The Cast option enables the usage of cast in the code. Finally, the ref option is used to enable optimization for reference parameters.
    • -wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,coq,tip: adds the different provers needed to verify the goals.
    • -wp-check-memory-model: Insert memory model hypotheses in the function contracts. Necessary as we use the ref memory model.
  • -cpp-extra-args=-I../include: adds the include directory of Paparazzi.
  • -cpp-extra-args=-DFRAMA_C_ANALYSIS: defines a C constant in order to remove certain portions of code that are not supported by Frama-C.

More information about Paparazzi

To have information about Paparazzi, go directly on the website or on the GitLab project.

Baptiste Pollien, PhD
Baptiste Pollien, PhD
Software Engineer HMI

I am a Software Engineer HMI at Ampere Software Technology.