B. Jacobs, J. Smans, and P. Philippaerts, VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, Nasa Formal Methods (NFM) (LNCS), pp.41-55, 2011.

F. Kirchner, N. Kosmatov, and V. Prevosto, Julien Signoles, and Boris Yakobowski. 2015. Frama-C: A software analysis perspective. Formal Asp. Comput, vol.27, pp.573-609, 2015.

N. Kosmatov and J. Signoles, A Lesson on Runtime Assertion Checking with Frama-C, Runtime Verification (RV), vol.8174, pp.386-399, 2013.
URL : https://hal.archives-ouvertes.fr/cea-01834991

K. Rustan, M. Leino, and M. Moskal, Usable Auto-Active Verification, 2010.

F. Loulergue, A. Blanchard, and N. Kosmatov, Ghosts for Lists: from Axiomatic to Executable Specifications, Proc. of the 12th International Conference on Tests and Proofs (TAP 2018) (LNCS), vol.10889, pp.177-184, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01811922

F. Mangano, S. Duquennoy, and N. Kosmatov, A Memory Allocation Module of Contiki Formally Verified with Frama-C. A Case Study, CRiSIS 2016, vol.10158, 2016.

W. Mansky, A. W. Appel, and A. Nogin, A Verified Messaging System, Proc. ACM Program. Lang. 1, OOPSLA, Article, vol.87, 2017.

A. Peyrard, N. Kosmatov, S. Duquennoy, and S. Raza, Towards Formal Verification of Contiki OS: Analysis of the AES-CCM* Modules with Frama-C, RED-IoT, 2018.

P. Philippaerts, J. T. Mühlberg, and W. Penninckx, Software verification with VeriFast: Industrial case studies, Science of Computer Programming, vol.82, pp.77-97, 2014.

N. Polikarpova, C. A. Furia, and B. Meyer, Specifying Reusable Components, Proc. of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2010), vol.6217, pp.127-141, 2010.

J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS), pp.55-74, 2002.

, The Coq Development Team

, The Coq Proof Assistant

F. Vogels, B. Jacobs, and F. Piessens, Featherweight VeriFast, Logical Methods in Computer Science, vol.11, p.19, 2015.

K. Q. Ye, M. Green, N. Sanguansin, L. Beringer, A. Petcher et al., Verified Correctness and Security of mbedTLS HMAC-DRBG, ACM SIGSAC Conference on Computer and Communications Security (CCS), 2007.