J. Abrial, The B-Book, assigning programs to meaning, 1996.

W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt et al., Deductive Software Verication -The KeY Book -From Theory to Practice, Lecture Notes in Computer Science, vol.10001, 2016.

M. Barnett, R. Deline, B. Jacobs, B. Chang, K. Rustan et al., Boogie: A Modular Reusable Verier for Object-Oriented Programs, Formal Methods for Components and Objects: 4th International Symposium, vol.4111, p.364387, 2005.

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

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 (STTT), vol.7, issue.3, p.212232, 2005.

B. Carré and J. Garnsworthy, SPARKan annotated Ada subset for safety-critical programming, Proceedings of the conference on TRI-ADA'90, TRI-Ada'90, p.392402, 1990.

A. Charguéraud, Characteristic formulae for the verication of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (ICFP), p.418430, 2011.

A. Charguéraud, J. Filliâtre, C. Lourenço, and M. Pereira, GOSPEL providing OCaml with a formal specication language, FM 2019 23rd International Symposium on Formal Methods, 2019.

A. Charguéraud and J. Filliâtre, Mário Pereira, and François Pottier. VOCAL A Veried OCaml Library. ML Family Workshop, 2017.

A. Charguéraud and F. Pottier, Verifying the correctness and amortized complexity of a union-nd implementation in separation logic with time credits, Journal of Automated Reasoning, vol.62, issue.3, p.331365, 2019.

M. Clochard, J. Filliâtre, and A. Paskevich, How to avoid proving the absence of integer overows, 7th Working Conference on Veried Software: Theories, Tools and Experiments (VSTTE), vol.9593, p.94109, 2015.

M. Dahlweid, M. Moskal, T. Santen, S. Tobies, and W. Schulte, VCC: Contract-based modular verication of concurrent C, 31st International Conference on Software Engineering, p.429430, 2009.

J. Filliâtre, Why3 where programs meet provers, KeY Symposium 2017, 2017.

J. Filliâtre, L. Gondelman, and A. Paskevich, A pragmatic type system for deductive verication, 2016.

J. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, Formal Methods in System Design, vol.48, issue.3, p.152174, 2016.

J. , C. Filliâtre, and A. Paskevich, Why3 where programs meet provers, Proceedings of the 22nd European Symposium on Programming, vol.7792, p.125128, 2013.

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx et al., VeriFast: A powerful, sound, predictable, fast verier for C and Java, NASA Formal Methods, vol.6617, p.4155, 2011.

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-veried C static analyzer, 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p.247259, 2015.

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-c: A software analysis perspective, Formal Aspects of Computing, vol.27, issue.3, p.573609, 2015.
URL : https://hal.archives-ouvertes.fr/cea-01808981

K. and R. M. Leino, Dafny: An automatic program verier for functional correctness, LPAR-16, vol.6355, p.348370, 2010.

X. Leroy, A formally veried compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, p.363446, 2009.

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verication system, 11th International Conference on Automated Deduction, p.748752, 1992.

M. Pereira, Tools and Techniques for the Verication of Modular Stateful Code, 2018.

N. Polikarpova, J. Tschannen, and C. A. Furia, A fully veried container library, Formal Asp. Comput, vol.30, issue.5, p.495523, 2018.

F. Pottier, Verifying a hash table and its iterators in higher-order separation logic, Proceedings of the 6th ACM SIGPLAN Conference on Certied Programs and Proofs, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01417102

M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, and T. Winterhalter, Coq coq correct! verication of type checking and erasure for coq, in coq, Proc. ACM Program. Lang, vol.4, 2019.

N. Swamy, C. Hriµcu, A. Keller, A. Rastogi, S. Delignat-lavaud et al., Dependent types and multi-monadic eects in F*, 43rd ACM Symposium on Principles of Programming Languages (POPL), p.256270, 2016.

, The Coq Development Team. The Coq Proof Assistant Reference Manual Version V8, vol.9, 2019.

J. Tschannen, C. A. Furia, M. Nordio, and N. Polikarpova, Autoproof: Auto-active functional verication of object-oriented programs, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2015.