C code + ACSL annotations --( Frama-C )--> "WhyML" Why3 format Proofs --( Why3 analyser )--> proven code
- ACSL By Example (good learning point with plenty of exmaples) Towards a Verified C Standard Library
https://www.mimuw.edu.pl/~alx/konstruowanie/ACSL-by-Example.pdf
- Frama-C code analyser (Framework for Modular Analysis of C programs)
https://frama-c.com/
https://frama-c.com/html/documentation.html
https://frama-c.com/2016/11/22/Frama-C-and-ACSL-are-on-GitHub.html
- Why3 / WhyML :
http://why3.lri.fr/doc/starting.html
