Commit b7b55dd7 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update Readme

parent ad08a5d4
......@@ -64,6 +64,10 @@ 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, lemma and logical functions for the
verification of functional properties.
- `sw/airborne/.frama-c/wp/interactive`: All the Coq scripts
containing the proof of certain lemma.
- `sw/airborne/.frama-c/wp/script`: All WP scripts containing
the tactics used to prove some goals.
The verification:
-----------------
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment