M. D. Aagaard, R. B. Jones, R. Kaivola, K. R. Kohatsu, and C. H. Seger, Formal verification of iterative algorithms in microprocessors, Proceedings Design Automation Conference (DAC 2000), pp.201-206, 2000.

J. R. Abrial, The B-book: assigning programs to meanings, 1996.

M. Barnett and K. R. Leino, Weakest-precondition of Unstructured Programs, SIGSOFT Softw. Eng. Notes, vol.31, issue.1, pp.82-87, 2005.

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi'c et al., CAV'11), vol.6806, pp.171-177, 2011.

C. Barrett, A. Stump, C. Tinelli, S. Boehme, D. Cok et al., The SMT-LIB, 2010.

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

R. Chapman, Industrial Experience with SPARK, Ada Letters XX, issue.4, 2000.

S. Conchon, A. Coquereau, M. Iguernlala, and A. Mebsout, Alt-Ergo 2.2, SMT Workshop: International Workshop on SMT, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01960203

L. De-moura and N. Bjorner, Z3: An Efficient SMT Solver, 2008.

E. W. Dijkstra, Guarded Commands, Nondeterminacy and Formal Derivation of Programs, ACM, vol.18, issue.8, pp.453-457, 1975.

B. Dutertre, Computer Aided Verification. 737-744, 2014.

W. E. Ferguson, Digit Serial Methods with Applications to Division and Square Root, IEEE Transactions on Computers, vol.67, issue.3, pp.449-456, 2018.

C. Flanagan, C. Flanagan, and J. B. Saxe, Avoiding Exponential Explosion: Generating Compact Verification Conditions, SIGPLAN Not, vol.36, issue.3, pp.193-205, 2001.

J. Harrison, Formal Verification of Square Root Algorithms, Formal Methods in System Design, vol.22, issue.2, pp.143-153, 2003.

C. A. Hoare, An Axiomatic Basis for Computer Programming, 1969.

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective, Formal Aspects of Computing, vol.27, issue.3, 2015.
URL : https://hal.archives-ouvertes.fr/cea-01808981

V. V. Kuliamin, Standardization and testing of implementations of mathematical functions in floating point numbers, Programming and Computer Software, vol.33, issue.3, pp.154-173, 2007.

L. Mauborgne, Astrée: Verification of Absence of Runtime Error, Building the Information Society: IFIP 18th World Computer Congress Topical Sessions 22-27, pp.385-392, 2004.

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

Y. Moy, E. Ledinot, H. Delseny, V. Wiels, and B. Monate, Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, IEEE Soft, vol.30, issue.3, 2013.

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 Computer-Aided Design, pp.149-152, 2016.

F. Randimbivololona, J. Souyris, P. Baudin, A. Pacalet, J. Raguideau et al., Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems, 1999.

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. M. Russinoff, A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division, and Square Root Algorithm of the AMDK7 Processor, J. Comput. Math. (UK), vol.1, 1998.

J. Sawada and R. Gamboa, Mechanical Verification of a Square Root Algorithm Using Taylor's Theorem, Lecture Notes in Computer Science, vol.2517, pp.274-291, 2002.

V. I. Shelekhov, Verification and synthesis of addition programs under the rules of correctness of statements, Automatic Control and Computer Sciences, vol.45, issue.7, pp.421-427, 2011.

N. V. Shilov, I. S. Anureev, and E. V. Bodin, Generation of correctness conditions for imperative programs, Programming and Computer Software, vol.34, issue.6, pp.307-321, 2008.

N. V. Shilov, D. A. Kondratyev, I. S. Anureev, E. V. Bodin, and A. V. Promsky, Platform-independent Specification and Verification of the Standard Mathematical Square Root Function. Modeling and Analysis of, Information Systems, vol.25, issue.6, pp.637-666, 2018.

V. Todorov, F. Boulanger, and S. Taha, Formal Verification of Automotive Embedded Software, Proceedings of the 6th Conference on Formal Methods in Software Engineering, vol.18, pp.84-87, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01768687