P. Baudin, J. Filliâtre, C. Marché, B. Monate, Y. Moy et al., ACSL: ANSI/ISO C Specification Language, version 1, 2009.

B. Beckert and M. Moskal, Deductive Verification of System Software in the Verisoft XT Project, KI - K??nstliche Intelligenz, vol.44, issue.1???2, pp.57-61, 2010.
DOI : 10.1007/s13218-010-0005-7

J. Bloch, Nearly all binary searches and mergesorts are broken, 2006.

F. Bobot, S. Conchon, É. Contejean, M. Iguernelala, S. Lescuyer et al., The Alt-Ergo automated theorem prover, 2008.

L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry et al., An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer, vol.box, issue.3, pp.212-232, 2005.
DOI : 10.1145/581376.581378

A. Charguéraud, Characteristic formulae for the verification of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), pp.418-430, 2011.

A. Sylvain-conchon, S. Goel, A. Krsti?, F. Mebsout, and . Zaïdi, Cubicle: A parallel SMT-based model checker for parameterized systems, CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification, 2012.

P. Cousot, R. Cousot, J. Feret, and L. Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The ASTRÉE analyzer, ESOP, number 3444 in Lecture Notes in Computer Science, pp.21-30, 2005.

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Proceedings of the 10th International Conference on Software Engineering and Formal Methods, number 7504 in Lecture Notes in Computer Science, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

L. De, M. , and N. Bjørner, Z3, an efficient SMT solver, TACAS, pp.337-340, 2008.

J. Filliâtre, Deductive software verification, International Journal on Software Tools for Technology Transfer, vol.21, issue.2, pp.397-403, 2011.
DOI : 10.1023/A:1005806324129

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.107-115, 2010.
DOI : 10.1145/1629575.1629596

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/978-3-642-59495-3
URL : https://hal.archives-ouvertes.fr/inria-00360768

N. Polikarpova, J. Tschannen, and C. A. Furia, A Fully Verified Container Library, FM 2015: Formal Methods -20th International Symposium Proceedings, pp.414-434, 2015.
DOI : 10.1007/978-3-319-19249-9_26

W. Schulte, S. Xia, and F. Piessens, A glimpse of a verifying C compiler

J. Tschannen, C. A. Furia, M. Nordio, and N. Polikarpova, AutoProof: Auto-Active Functional Verification of Object-Oriented Programs, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, 2015.
DOI : 10.1007/978-3-662-46681-0_53