A. W. Appel, Verified Software Toolchain, Programming Languages and Systems (ESOP), vol.6602, pp.1-17, 2011.

A. W. Appel, Verification of a Cryptographic Primitive, p.256, 2015.

, ACM Trans. Program. Lang. Syst, vol.37, issue.7, pp.1-7, 2015.

A. W. Appel, R. Dockins, A. Hobor, L. Beringer, J. Dodds et al., Program Logics for Certified Compilers, 2014.

P. Baudin, P. Cuoq, J. Filliâtre, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language, 2018.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

A. Blanchard, N. Kosmatov, and F. Loulergue, Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C, Proc. of the 10th NASA Formal Methods Symposium (NFM 2018), vol.10811, pp.37-53, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01720401

J. Burghardt and J. Gerlach, , 2018.

Á. Darvas and P. Müller, Proving Consistency and Completeness of Model Classes Using Theory Interpretation, Proc. of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE 2010), vol.6013, pp.218-232, 2010.

C. Dross and Y. Moy, Auto-Active Proof of Red-Black Trees in SPARK, NASA Formal Methods -9th International Symposium, pp.68-83, 2017.

A. Dunkels, B. Gronvall, and T. Voigt, Contiki -A Lightweight and Flexible Operating System for Tiny Networked Sensors, 2004.

J. , C. Filliâtre, and A. Paskevich,

, Why3 -Where Programs Meet Provers, ESOP 2013

C. Gladisch and S. Tyszberowicz, Specifying linked data structures in JML for combining formal verification and testing, Science of Computer Programming, pp.19-40, 2015.

P. Herms, C. Marché, and B. Monate, A Certified Multiprover Verification Condition Generator, Verified Software: Theories, Tools, Experiments (VSTTE), vol.7152, pp.2-17, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00639977

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.