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

L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. 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

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

D. Monniaux, Analyse statique : de la théorie à 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, In: FMICS. LNCS, vol.5825, pp.53-69, 2009.
DOI : 10.1007/978-3-642-04570-7_6

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.

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, 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

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. 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

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

J. C. 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

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

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

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

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

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.