J. Harrison, Formal verification of square root algorithms, Formal Methods in System Design, vol.22, issue.2, pp.143-153, 2003.

D. M. Russinoff, A mechanically checked proof of correctness of the AMD K5 floating point square root microcode, Formal Methods in System Design, vol.14, issue.1, pp.75-125, 1999.

D. L. Rager, J. Ebergen, D. Nadezhin, A. Lee, C. K. Chau et al., Formal verification of division and square root implementations, an Oracle report, 16th Conference on Formal Methods in ComputerAided Design, pp.149-152, 2016.

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

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

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

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, ser. LNCS, vol.10712, pp.84-101, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01519732