R. Affeldt, On Construction of a Library of Formally Verified Low-level Arithmetic Functions, Innovations in Systems and Software Engineering, vol.9, pp.59-77, 2013.

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

Y. Bertot, N. Magaud, and P. Zimmermann, A Proof of GMP Square Root, Journal of Automated Reasoning, vol.29, pp.225-252, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00101044

F. Bobot, J. 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

J. Filliâtre, One Logic To Use Them All, 24th International Conference on Automated Deduction, vol.7898, pp.1-20, 2013.

J. Filliâtre, L. Gondelman, and A. Paskevich, The Spirit of Ghost Code, Formal Methods in System Design, vol.48, pp.152-174, 2016.

J. , C. Filliâtre, and A. Paskevich, Why3 -Where Programs Meet Provers, 22nd European Symposium on Programming, vol.7792, pp.125-128, 2013.

S. Fischer, Formal Verification of a Big Integer Library, DATE Workshop on Dependable Software Systems, 2008.

R. W. Floyd, Assigning Meanings to Programs, Program Verification, pp.65-81, 1993.

G. Melquiond and R. Rieu-helft, A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms, 9th International Joint Conference on Automated Reasoning, vol.10900, pp.178-193, 2018.

G. Melquiond and R. Rieu-helft, Formal Verification of a State-of-the-Art Integer Square Root, IEEE 26th Symposium on Computer Arithmetic, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02092970

N. Moller and T. Granlund, Improved Division by Invariant Integers, IEEE Trans. Comput, vol.60, pp.165-175, 2011.

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, vol.8307, pp.66-81, 2013.

R. Rieu-helft, A Why3 Proof of GMP Algorithms, Journal of Formalized Reasoning, vol.12, pp.53-97, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02477578

R. Rieu-helft, C. Marché, and G. Melquiond, How to Get an Efficient yet Verified Arbitrary-Precision Integer Library, 9th Working Conference on Verified Software: Theories, Tools, and Experiments, vol.10712, pp.84-101, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01519732

N. Schirmer, A Verification Environment for Sequential Imperative Programs in Isabelle/HOL, International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp.398-414, 2005.

M. Schoolderman, Verifying Branch-Free Assembly Code in Why3, Working Conference on Verified Software: Theories, Tools, and Experiments, pp.66-83, 2017.

J. Karim-zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, HACL*: A Verified Modern Cryptographic Library. Cryptology ePrint Archive, 2017.