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

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

S. Boldo and J. C. 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

S. Boldo and G. Melquiond, Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd, IEEE Transactions on Computers, vol.57, issue.4, pp.462-471, 2008.
DOI : 10.1109/TC.2007.70819
URL : https://hal.archives-ouvertes.fr/inria-00080427

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

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

N. Brisebarre, J. M. 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

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

W. D. Clinger, How to read floating-point numbers accurately, Programming Language Design and Implementation (PLDI'90), pp.92-101, 1990.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRE?? Analyzer, The ASTRÉEASTR´ASTRÉE analyzer. In: 14th European Symposium on Programming (ESOP), pp.21-30, 2005.
DOI : 10.1007/978-3-540-31987-0_3

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

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

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

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

T. Granlund and P. L. Montgomery, Division by invariant integers using multiplication, Programming Language Design and Implementation (PLDI'94), pp.61-72, 1994.

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

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

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

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

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

X. Leroy, The CompCert verified compiler, software and commented proof, 2014.

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

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

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

J. S. Moore, A mechanically verified language implementation, Journal of Automated Reasoning, vol.5, issue.4, pp.461-492, 1989.
DOI : 10.1007/BF00243133

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

T. M. Nguyen and C. Marché, Hardware-Dependent Proofs of Numerical Programs, International Conference on Certified Programs and Proofs (CPP), pp.314-329, 2011.
DOI : 10.1112/S1461157000000176
URL : https://hal.archives-ouvertes.fr/hal-00772508

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

S. Rump, T. Ogita, and S. Oishi, Accurate Floating-Point Summation Part I: Faithful Rounding, SIAM Journal on Scientific Computing, vol.31, issue.1, pp.189-224, 2008.
DOI : 10.1137/050645671

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

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

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), pp.283-294, 2011.