Formal verification of square root algorithms, Formal Methods in System Design, vol.22, issue.2, pp.143-153, 2003. ,
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. ,
Formal verification of division and square root implementations, an Oracle report, 16th Conference on Formal Methods in ComputerAided Design, pp.149-152, 2016. ,
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
Why3 -where programs meet provers, 22nd European Symposium on Programming, ser. LNCS, vol.7792, pp.125-128, 2013. ,
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
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