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

R. Affeldt, On construction of a library of formally verified low-level arithmetic functions, Innovations in Systems and Software Engineering, vol.375, issue.1???3, pp.59-77, 2013.
DOI : 10.1016/j.tcs.2006.12.036

S. Berghofer, Verification of dependable software using SPARK and Isabelle, 6th International Workshop on Systems Software Verification. OpenAccess Series in Informatics (OASIcs), pp.15-31, 2012.

Y. Bertot, N. Magaud, and P. Zimmermann, A proof of GMP square root, Journal of Automated Reasoning, vol.2934, pp.225-252, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00101044

F. Bobot, J. C. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

F. Bobot, J. C. Filliâtre, C. Marché, and A. Paskevich, Let???s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.7, issue.5, pp.709-727, 2015.
DOI : 10.1007/978-3-642-02959-2_10

R. Bornat, Proving Pointer Programs in Hoare Logic, Mathematics of Program Construction, pp.102-126, 2000.
DOI : 10.1007/10722010_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.7008

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 No. 7504 in Lecture Notes in Computer Science, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

J. C. Filliâtre, One logic to use them allCADE-24), 24th International Conference on Automated Deduction, pp.1-20, 2013.

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

J. C. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code, Formal Methods in System Design, vol.20, issue.2, pp.152-174, 2016.
DOI : 10.1007/978-3-319-08867-9_1

J. C. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

J. C. 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

S. Fischer, Formal verification of a big integer library In: DATE Workshop on Dependable Software Systems, 2008.

C. Fumex, C. Dross, J. Gerlach, and C. Marché, Specification and Proof of High-Level Functional Properties of Bit-Level Programs, 8th NASA Formal Methods Symposium, pp.291-306, 2016.
DOI : 10.1007/978-3-540-78800-3_24
URL : https://hal.archives-ouvertes.fr/hal-01314876

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

N. Kosmatov, C. Marché, Y. Moy, and J. Signoles, Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014, 7th International Symposium on Leveraging Applications of Formal Methods, pp.461-478, 2016.
DOI : 10.1007/978-3-662-46681-0_53
URL : https://hal.archives-ouvertes.fr/hal-01344110

K. R. Leino and M. Moskal, Usable auto-active verification, 2010.

N. Moller and T. Granlund, Improved Division by Invariant Integers, IEEE Transactions on Computers, vol.60, issue.2, pp.165-175, 2011.
DOI : 10.1109/TC.2010.143

M. O. Myreen and G. Curello, Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code, 3rd International Conference on Certified Programs and Proofs (CPP). Lecture Notes in Computer Science, pp.66-81, 2013.
DOI : 10.1007/978-3-319-03545-1_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.407.6661

J. K. Zinzindohoué, E. I. Bartzia, and K. Bhargavan, A Verified Extensible Library of Elliptic Curves, 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp.296-309, 2016.
DOI : 10.1109/CSF.2016.28