G. Barrett, Formal methods applied to a floating-point number system, IEEE Transactions on Software Engineering, vol.15, issue.5, pp.611-621, 1989.
DOI : 10.1109/32.24710

S. Boldo, Preuves formelles en arithmétiquesarithmétiques`arithmétiquesà virgule flottante, 2004.

S. Boldo and M. Daumas, Representable correcting terms for possibly underflowing floating point operations, 16th IEEE Symposium on Computer Arithmetic, 2003. Proceedings., pp.79-86, 2003.
DOI : 10.1109/ARITH.2003.1207663

S. Boldo and M. Daumas, A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials, Numerical Algorithms, vol.37, issue.1-4, pp.45-60, 2004.
DOI : 10.1023/B:NUMA.0000049487.98618.61

W. J. Cody and R. Karpinski, A Proposed Radix- and Word-length-independent Standard for Floating-point Arithmetic, IEEE Micro, vol.4, issue.4, pp.86-100, 1984.
DOI : 10.1109/MM.1984.291224

T. Coe, Inside the Pentium FDIV bug. Dr. Dobb's, Journal, vol.20, issue.148, pp.129-135, 1995.

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001.
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285

T. J. Dekker, A floating-point technique for extending the available precision, Numerische Mathematik, vol.5, issue.3, pp.224-242, 1971.
DOI : 10.1007/BF01397083

C. T. Fike, Methods of evaluating polynomial approximations in function evaluation routines, Communications of the ACM, vol.10, issue.3, pp.175-178, 1967.
DOI : 10.1145/363162.363200

D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-47, 1991.
DOI : 10.1145/103162.103163
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.7712

J. Harrison, Floating point verification in HOL light: The exponential function, 1997.
DOI : 10.1007/BFb0000475

J. Harrison, Verifying the accuracy of polynomial approximations in HOL, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, pp.137-152, 1997.
DOI : 10.1007/BFb0028391

J. Harrison, A Machine-Checked Theory of Floating Point Arithmetic, 12th International Conference on Theorem Proving in Higher Order Logics, pp.113-130, 1999.
DOI : 10.1007/3-540-48256-3_9

J. Harrison, Formal Verification of Floating Point Trigonometric Functions
DOI : 10.1007/3-540-40922-X_14

N. J. Higham and C. Jacobi, Accuracy and stability of numerical algorithms Formal Verification of a Fully IEEE Compliant Floating Point Unit, SIAM, 2002.

W. Kahan, Mathematics written in sand?the HP-15C, Intel 8087, etc, Statistical Computing Section, Proceedings of the American Statistical Association, pp.12-26, 1983.

C. Kern and M. R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems, vol.4, issue.2, pp.123-193, 1999.
DOI : 10.1145/307988.307989

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

X. S. Li, J. W. Demmel, D. H. Bailey, G. Henry, Y. Hida et al., Design, implementation and testing of extended and mixed precision BLAS, ACM Transactions on Mathematical Software, vol.28, issue.2, pp.152-205, 2002.
DOI : 10.1145/567806.567808

P. S. Miner and J. F. Leathrum, Verification of IEEE compliant subtractive division algorithms, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, pp.64-78, 1996.
DOI : 10.1007/BFb0031800

J. Muller, On the definition of ulp(x), 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070503

J. O. Leary, X. Zhao, R. Gerth, and C. H. Seger, Formally verifying IEEE compliance of floating point hardware, Intel Technology Journal, vol.3, issue.1, 1999.

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, 11th International Conference on Automated Deduction (CADE), pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.2627

D. M. Russinoff, Abstract, LMS Journal of Computation and Mathematics, vol.11, pp.148-200, 1998.
DOI : 10.1112/S1461157000000176

D. M. Russinoff, A mechanically checked proof of correctness of the AMD-K5 floating point square root microcode. Formal Methods in System Design, p.75, 1999.

D. M. Russinoff, A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor, Lecture Notes in Computer Science, pp.3-36, 1954.
DOI : 10.1007/3-540-40922-X_3

P. H. Sterbenz, Floating point computation, 1974.

D. Stevenson, A Proposed Standard for Binary Floating-Point Arithmetic, Computer, vol.14, issue.3, pp.51-62, 1981.
DOI : 10.1109/C-M.1981.220377

D. Stevenson, An American national standard: IEEE standard for binary floating point arithmetic