, Ensure: value(a, n) = value(s, n/2 + 1) 2 + value(r, result) Ensure: value(r, result) ? 2 × value(s, n) Ensure: result > 0 ? r

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, 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, issue.3-4, 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

M. Bodrato and A. Zanoni, Integer and polynomial multiplication: Towards optimal Toom-Cook matrices, 2007 International Symposium on Symbolic and Algebraic Computation, pp.17-24, 2007.

P. Richard, P. Brent, and . Zimmermann, Modern Computer Arithmetic, 2010.

M. Clochard, Preuves taillées en biseau, vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), 2017.

A. Stephen and . Cook, On the minimum computation time of functions, 1966.

M. Daumas and G. Melquiond, Certification of bounds on expressions involving rounded operators, Transactions on Mathematical Software, vol.37, issue.1, pp.1-20, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00127769

W. Edsger and . Dijkstra, A discipline of programming, vol.1, 1976.

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, issue.3, 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.

L. Gondelman, A Pragmatic Type System for Deductive Software Verification, 2016.
URL : https://hal.archives-ouvertes.fr/tel-01533090

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

A. Karatsuba, Multiplication of multidigit numbers on automata, Soviet Physics Doklady, vol.7, pp.595-596, 1963.

D. E. Knuth, The Art of Computer Programming, Seminumerical Algorithms, vol.2, 1997.

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, number 10900 in Lecture Notes in Computer Science, pp.178-193, 2018.

G. Melquiond and R. Rieu-helft, Formal verification of a state-of-theart integer square root, IEEE 26th Symposium on Computer Arithmetic (ARITH), 2019.

N. Moller and T. Granlund, Improved division by invariant integers, IEEE Transactions on Computers, 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, 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.

A. L. Toom, The complexity of a scheme of functional elements realizing the multiplication of integers, Soviet Mathematics Doklady, vol.3, pp.714-716, 1963.

H. S. Warren, Hacker's Delight, 2012.

J. Karim-zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, HACL*: A verified modern cryptographic library. Cryptology ePrint Archive, 2017.