A. Ayad and C. Marché, Multi-prover verification of floating-point programs, Fifth International Joint Conference on Automated Reasoning, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00534333

M. Barnett, K. R. Leino, and W. Schulte, The spec# programming system: an overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS'04), Lecture Notes in Computer Science, vol.3362, pp.49-69, 2004.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

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

S. Boldo, Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms, Third International Joint Conference on Automated Reasoning, pp.52-66, 2006.

S. Boldo, Floats & Ropes: a case study for formal numerical program verification, 36th International Colloquium on Automata, Languages and Programming, pp.91-102, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00432718

S. Boldo, Kahan's algorithm for a correct discriminant computation at last formally proven, IEEE Trans. Comput, vol.58, issue.2, pp.220-225, 2009.

S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Formal proof of a wave equation resolution scheme: the method error, Proceedings of the First Interactive Theorem Proving Conference, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00450789

S. Boldo, M. Daumas, W. Kahan, and G. Melquiond, Proof and certification for an accurate discriminant, 12th IMACS-GAMM International Symposium on Scientific Computing, 2006.

S. Boldo and J. Filliâtre, Formal verification of floating-point programs, 18th IEEE International Symposium on Computer Arithmetic, pp.187-194, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01174892

S. Boldo, J. Filliâtre, and G. Melquiond, Combining Coq and Gappa for certifying floating-point programs, 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, pp.59-74, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00432726

S. Boldo and T. M. Nguyen, Hardware-independent proofs of numerical programs, Proceedings of the Second NASA Formal Methods Symposium. number NASA/CP-2010-216215 in NASA Conference Publication, pp.14-23, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00534410

S. Boldo and T. M. Nguyen, Proofs of numerical programs when the compiler optimizes, Innov. Syst. Softw. Eng, vol.7, pp.1-10, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00777639

L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry et al., An overview of JML tools and applications, Int. J. Softw. Tools Technol. Transf. (STTT), vol.7, issue.3, pp.212-232, 2005.

B. Carré and J. Garnsworthy, SPARK?an annotated Ada subset for safety-critical programming, Proceedings of the Conference on TRI-ADA'90, TRI-Ada'90, pp.392-402, 1990.

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

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRÉE analyzer, In: ESOP. Lecture Notes in Computer Science, vol.3444, pp.21-30, 2005.

M. Daumas, L. Rideau, and L. Théry, A generic library of floating-point numbers and its application to exact computing, 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001.

T. J. Dekker, A floating point technique for extending the available precision, Numerische Mathematik, vol.18, issue.3, pp.224-242, 1971.

D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal et al., Towards an industrial use of FLUCTUAT on safety-critical avionics software, FMICS, LNCS, pp.53-69, 2009.

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus platform for deductive program verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007.

J. Gerlach and J. Burghardt, An experience report on the verification of algorithms in the c++ standard library using frama-c, Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, pp.191-204, 2010.

E. Goubault and S. Putot, Static analysis of numerical algorithms, ) SAS. LNCS, pp.18-34, 2006.

J. Harrison, Formal verification of floating point trigonometric functions, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, pp.217-233, 2000.

N. J. Higham, Accuracy and stability of numerical algorithms, 2002.

W. Kahan, On the cost of Floating-Point Computation Without Extra-Precise Arithmetic. World-Wide Web document, 2004.

G. T. Leavens, Not a number of floating point problems, J. Object Technol, vol.5, issue.2, pp.75-83, 2006.

G. Melquiond, Floating-point arithmetic in the Coq system, Proceedings of the 8th Conference on Real Numbers and Computers, pp.93-102, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00797913

G. Melquiond, Proving bounds on real-valued functions with computations, Proceedings of the 4th International Joint Conference on Automated Reasoning, pp.2-17, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00180138

D. Monniaux, Analyse statique : de la théorie à la pratique. Habilitation to direct research Université Joseph Fourier, 2009.

Y. Moy and C. Marché, Jessie Plugin Tutorial, Beryllium version, INRIA, 2009.

Y. Moy and C. Marché, Modular inference of subprogram contracts for safety checking, J. Symb. Comput, vol.45, pp.1184-1211, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00534331

G. C. Necula, S. Mcpeak, S. P. Rahul, and W. Weime, Cil: Intermediate language and tools for analysis and transformation of c programs, Conference on Compiler Construction (CC'02), 2002.

D. M. Russinoff, A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor, LMS J. Comput. Math, vol.1, pp.148-200, 1998.

P. H. Sterbenz, Floating Point Computation, Upper Saddle River, 1974.

G. W. Veltkamp, Algolprocedures voor het berekenen van een inwendig product in dubbele precisie, RC-Informatie Technische Hogeschool Eindhoven, vol.22, 1968.

J. H. Wilkinson, Rounding Errors in Algebraic Processes, 1963.