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

M. Barnett, K. Leino, K. Rustan, M. Leino, and W. Schulte, The Spec# Programming System: An Overview, pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.2133

P. Baudin, J. Filliâtre, C. Marché, B. Monate, Y. Moy et al., ACSL: ANSI/ISO C Specification Language, 2008.

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

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.
DOI : 10.1109/TC.2008.200
URL : https://hal.archives-ouvertes.fr/inria-00432726

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

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry et al., An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer, vol.box, issue.3, pp.212-232, 2005.
DOI : 10.1007/s10009-004-0167-4

V. Carreño and P. 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.

S. Conchon, E. Contejean, and J. Kanig, CC(X): Efficiently Combining Equality and Solvable Theories without Canonizers, SMT 2007?5th International Workshop on Satisfiability Modulo, 2007.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRE?? Analyzer, ESOP, no. 3444 in LNCS, pp.21-30, 2005.
DOI : 10.1007/978-3-540-31987-0_3

M. Daumas and G. Melquiond, Certification of bounds on expressions involving rounded operators, ACM Transactions on Mathematical Software, vol.37, issue.1, pp.1-220, 2010.
DOI : 10.1145/1644001.1644003
URL : https://hal.archives-ouvertes.fr/hal-00127769

M. Daumas, G. Melquiond, and C. Muñoz, Guaranteed Proofs Using Interval Arithmetic, 17th IEEE Symposium on Computer Arithmetic (ARITH'05), pp.188-195, 2005.
DOI : 10.1109/ARITH.2005.25
URL : https://hal.archives-ouvertes.fr/hal-00164621

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.
DOI : 10.1007/978-3-642-04570-7_6

G. Dowek, C. Muñoz, and V. Carreño, Provably Safe Coordinated Strategy for Distributed Conflict Resolution, AIAA Guidance, Navigation, and Control Conference and Exhibit, pp.2005-6047, 2005.
DOI : 10.2514/6.2005-6047

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, Computer Aided Verification (CAV), pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

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, Formal Verification of Floating Point Trigonometric Functions, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, pp.217-233, 2000.
DOI : 10.1007/3-540-40922-X_14

N. Higham, Accuracy and stability of numerical algorithms, 2002.
DOI : 10.1137/1.9780898718027
URL : http://eprints.ma.man.ac.uk/238/04/covered/MIMS_ep2006_75_Book_Covers.pdf

J. Language, http://www.jmlspecs.org 21 Not a number of floating point problems, Leavens GT J Object Technol, vol.5, issue.2, pp.75-83, 2006.

. Microprocessor-standards-subcommittee, IEEE Standard for Floating-Point Arithmetic, p.4610935, 2008.

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

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

T. Ogita, S. Rump, and S. Oishi, Accurate Sum and Dot Product, SIAM Journal on Scientific Computing, vol.26, issue.6, pp.1955-1988, 2005.
DOI : 10.1137/030601818
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.1547

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