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

F. Bobot, É. Sylvain-conchon, and . Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008.

B. Carré and J. Garnsworthy, SPARK-an annotated Ada subset for safety-critical programming, Proceedings of the conference on TRI-ADA'90, TRI-Ada'90, pp.392-402, 1990.

R. Cauderlier and M. Sighireanu, A verified implementation of the bounded list container, Tools and Algorithms for the Construction and Analysis of Systems, pp.172-189, 2018.

A. Charguéraud, Characteristic Formulae for Mechanized Program Verification, 2010.

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. Charguéraud and F. Pottier, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Journal of Automated Reasoning, 2017.

A. Charguéraud and F. Pottier, Temporary read-only permissions for separation logic, Proceedings of the European Symposium on Programming, 2017.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRÉE analyzer, ESOP, number 3444 in Lecture Notes in Computer Science, pp.21-30, 2005.

S. Cruanes, R. Grinberg, J. Deplaix, and J. M. Qcheck, , 2019.

. Stijn-de-gouw, . Frank-s-de, R. Boer, R. Bubel, J. Hähnle et al., Verifying openjdk's sort method for generic collections, Journal of Automated Reasoning, 2017.

J. Filliâtre, One logic to use them all, 24th International Conference on Automated Deduction, vol.7898, pp.1-20, 2013.

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

A. Guéneau, A. Charguéraud, and F. Pottier, A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification, ESOP 2018 -27th European Symposium on Programming, vol.10801, 2018.

J. Hatcliff, G. T. Leavens, K. Rustan, M. Leino, P. Müller et al., Behavioral interface specification languages, ACM Comput. Surv, vol.44, issue.3, 2012.

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx et al., VeriFast: A powerful, sound, predictable, fast verifier for C and Java, NASA Formal Methods, vol.6617, pp.41-55, 2011.

I. T. Kassios, Tutorial for the 2nd COST Action IC0701 Training School, Limerick 6/11, 2011.

I. T. Kassios, The dynamic frames theory, Formal Aspects of Computing, vol.23, issue.3, pp.267-288, 2011.

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, pp.573-609, 2015.
URL : https://hal.archives-ouvertes.fr/cea-01808981

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4: Formal verification of an OS kernel, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.

N. Kosmatov, C. Marché, Y. Moy, and J. Signoles, Static versus dynamic verification in Why3, Frama-C and SPARK, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), vol.9952, pp.461-478, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01344110

T. Gary, A. L. Leavens, C. Baker, and . Ruby, Preliminary design of JML: A behavioral interface specification language for Java, 2000.

K. and R. M. Leino, Dafny: An automatic program verifier for functional correctness, LPAR-16, vol.6355, pp.348-370, 2010.

K. Rustan, M. Leino, and P. Müller, A basis for verifying multi-threaded programs, Programming Languages and Systems, pp.378-393, 2009.

X. Leroy, A formally verified compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, pp.363-446, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00360768

P. Müller, M. Schwerhoff, and A. J. Summers, Viper: A verification infrastructure for permission-based reasoning, Verification, Model Checking, and Abstract Interpretation (VMCAI), vol.9583, pp.41-62, 2016.

G. Mével, J. Jourdan, and F. Pottier, Time credits and time receipts in Iris, European Symposium on Programming, vol.11423, pp.1-27, 2019.

J. Matthew, A. J. Parkinson, and . Summers, The relationship between separation logic and implicit dynamic frames, Logical Methods in Computer Science, vol.8, issue.3, 2012.

M. Pereira, Tools and Techniques for the Verification of Modular Stateful Code, 2018.
URL : https://hal.archives-ouvertes.fr/tel-01980343

N. Polikarpova, J. Tschannen, and C. A. Furia, A fully verified container library, Formal Asp. Comput, vol.30, issue.5, pp.495-523, 2018.

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, 17th Annual IEEE Symposium on Logic in Computer Science, 2002.

J. Signoles, N. Kosmatov, and K. Vorobyov, E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs. Tool Paper, International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES'17), 2017.

J. Smans, B. Jacobs, and F. Piessens, Implicit dynamic frames: Combining dynamic frames and separation logic, ECOOP 2009 -Object-Oriented Programming, pp.148-172, 2009.

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