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

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

. Microprocessor-standards-subcommittee, IEEE Standard for Floating- Point Arithmetic, IEEE Std, pp.754-2008, 2008.

V. A. Carreño and P. S. Miner, Specification of the IEEE-854 floatingpoint standard in HOL and PVS, HOL95: 8th International Workshop on Higher-Order Logic Theorem Proving and Its Applications, 1995.

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

J. Harrison, Formal Verification of Floating Point Trigonometric Functions, 3rd International Conference on Formal Methods in Computer- Aided Design, pp.217-233, 2000.
DOI : 10.1007/3-540-40922-X_14

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

S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011.
DOI : 10.1109/ARITH.2011.40
URL : https://hal.archives-ouvertes.fr/inria-00534854

D. Monniaux, The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, p.12, 2008.
DOI : 10.1145/1353445.1353446
URL : https://hal.archives-ouvertes.fr/hal-00128124

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and understanding bugs in C compilers, 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp.283-294, 2011.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRÉEASTR´ASTRÉE analyzer, ESOP, ser, pp.21-30, 2005.

]. D. Monniaux, Analyse statique : de la théoriè a la pratique Habilitation to direct research, 2009.

D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal et al., Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software, FMICS, ser. LNCS, pp.53-69, 2009.
DOI : 10.1007/978-3-642-04570-7_6

G. T. Leavens, Not a Number of Floating Point Problems., The Journal of Object Technology, vol.5, issue.2, pp.75-83, 2006.
DOI : 10.5381/jot.2006.5.2.c8

S. Boldo and J. Filliâtre, Formal Verification of Floating-Point Programs, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.187-194, 2007.
DOI : 10.1109/ARITH.2007.20
URL : https://hal.archives-ouvertes.fr/hal-01174892

A. Ayad and C. Marché, Multi-Prover Verification of Floating-Point Programs, 5th International Joint Conference on Automated Reasoning, 2010.
DOI : 10.1007/978-3-642-14203-1_11
URL : https://hal.archives-ouvertes.fr/inria-00534333

S. Boldo and T. M. Nguyen, Proofs of numerical programs when the compiler optimizes, Innovations in Systems and Software Engineering, pp.151-160, 2011.
DOI : 10.1007/s11334-011-0151-6
URL : https://hal.archives-ouvertes.fr/hal-00777639

T. M. Nguyen and C. Marché, Hardware-Dependent Proofs of Numerical Programs, Certified Programs and Proofs, ser. Lecture Notes in Computer Science, 2011.
DOI : 10.1112/S1461157000000176
URL : https://hal.archives-ouvertes.fr/hal-00772508

R. Milner and R. Weyhrauch, Proving compiler correctness in a mechanized logic, " in 7th Annual Machine Intelligence Workshop, ser. Machine Intelligence, pp.51-72, 1972.

J. S. Moore, A mechanically verified language implementation, Journal of Automated Reasoning, vol.5, issue.4, pp.461-492, 1989.
DOI : 10.1007/BF00243133
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.604

G. Li, S. Owens, and K. Slind, Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic, 16th European conference on Programming, ser. ESOP'07, pp.205-219, 2007.
DOI : 10.1007/978-3-540-71316-6_15

M. O. Myreen, Formal verification of machine-code programs, 2008.

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

J. Nickolls and W. Dally, The GPU Computing Era, IEEE Micro, vol.30, issue.2, pp.56-69, 2010.
DOI : 10.1109/MM.2010.41

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

W. D. Clinger, How to read floating-point numbers accurately, Programming Language Design and Implementation (PLDI'90, pp.92-101, 1990.
DOI : 10.1145/989393.989430
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.164.813

S. A. Figueroa, When is double rounding innocuous?, ACM SIGNUM Newsletter, vol.30, issue.3, pp.21-26, 1995.
DOI : 10.1145/221332.221334

N. Brisebarre, J. Muller, and S. K. Raina, Accelerating correctly rounded floating-point division when the divisor is known in advance, IEEE Transactions on Computers, vol.53, issue.8, pp.1069-1072, 2004.
DOI : 10.1109/TC.2004.37

A. Ioualalen and M. Martel, A New Abstract Domain for the Representation of Mathematically Equivalent Expressions, Static Analysis -19th International Symposium, SAS 2012, pp.75-93, 2012.
DOI : 10.1007/978-3-642-33125-1_8
URL : https://hal.archives-ouvertes.fr/hal-00698618