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

R. Bagnara, M. Carlier, R. Gori, and A. Gotlieb, Exploiting Binary Floating-Point Representations for Constraint Propagation, INFORMS Journal on Computing, vol.28, issue.1, pp.31-46, 2016.
DOI : 10.1287/ijoc.2015.0663
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.697.4460

S. Baird, A. Charlet, Y. Moy, and T. S. Taft, CodePeer ? beyond bug-finding with static analysis, Static Analysis of Software: the Abstract Interpretation, 2013.

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Let???s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.7, issue.5, pp.709-727, 2015.
DOI : 10.1007/s10009-014-0314-5
URL : http://hal.inria.fr/docs/00/96/71/32/PDF/main.pdf

S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.200, issue.25???28, pp.423-456, 2013.
DOI : 10.1007/s10817-012-9255-4
URL : https://hal.archives-ouvertes.fr/hal-00649240

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 and C. Marché, Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs, Mathematics in Computer Science, vol.1, issue.2, pp.377-393, 2011.
DOI : 10.1007/s11786-011-0099-9
URL : https://hal.archives-ouvertes.fr/hal-00777605

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, T. M. , and T. 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

M. Brain, D. Vijay, A. Griggio, L. Haller, and D. Kroening, Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods in System Design, pp.213-245, 2014.
DOI : 10.1007/s10703-013-0203-7
URL : http://dx.doi.org/10.1007/s10703-013-0203-7

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

R. Chapman and F. Schanda, Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK, Interactive Theorem Proving -5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 Proceedings, volume 8558 of Lecture Notes in Computer Science, pp.17-26, 2014.
DOI : 10.1007/978-3-319-08970-6_2

M. Sylvain-conchon, K. Iguernlala, G. Ji, C. Melquiond, and . Fumex, A three-tier strategy for reasoning about floating-point numbers in SMT, Computer Aided Verification, 2017.

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Proceedings of the 10th International Conference on Software Engineering and Formal Methods, number 7504 in Lecture Notes in Computer Science, pp.233-247, 2012.
DOI : 10.1007/978-3-642-33826-7_16

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

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001.
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285

L. De, M. , and N. Bjørner, Z3, an efficient SMT solver, TACAS, pp.337-340, 2008.

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

C. Dross and Y. Moy, Abstract Software Specifications and Automatic Proof of Refinement, 1st International Conference on Reliability, Safety and Security of Railway Systems, 2016.
DOI : 10.1007/978-3-319-33951-1_16

C. Dross and Y. Moy, Auto-Active Proof of Red-Black Trees in SPARK, NASA Formal Methods, 2017.
DOI : 10.1007/978-3-319-19249-9_26

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.
DOI : 10.1007/978-3-540-73368-3_21

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

C. Fumex, C. Dross, J. Gerlach, and C. Marché, Specification and proof of highlevel functional properties of bit-level programs, 8th NASA Formal Methods Symposium, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01314876

D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-48, 1991.
DOI : 10.1145/103162.103163
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.7712

A. Goodloe, C. A. Muñoz, F. Kirchner, and L. Correnson, Verification of Numerical Programs: From Real Numbers to Floating Point Numbers, NASA Formal Methods, 5th International Symposium, pp.441-446, 2013.
DOI : 10.1007/978-3-642-38088-4_31

J. Harrison, Floating point verification in HOL Light: The exponential function. Formal Methods in System Design, pp.271-305, 2000.
DOI : 10.1007/bfb0000475
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.5528

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, 1954.
DOI : 10.1007/3-540-40922-X_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.1426

J. Harrison, Floating-point verification, International Symposium of Formal Methods Europe, pp.529-532, 2005.
DOI : 10.1007/11526841_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.1549

N. Kosmatov, C. Marché, Y. Moy, and J. Signoles, Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp.461-478, 2016.
DOI : 10.1007/978-3-662-46681-0_53
URL : https://hal.archives-ouvertes.fr/hal-01344110

K. Rustan, M. Leino, and M. Moskal, Usable auto-active verification, Usable Verification Workshop, 2010.

C. Marché, Verification of the functional behavior of a floating-point program: An industrial case study, Science of Computer Programming, vol.96, issue.3, pp.279-296, 2014.
DOI : 10.1016/j.scico.2014.04.003

B. Marre and C. Michel, Improving the Floating Point Addition and Subtraction Constraints, Proceedings of the 16th International Conference on Principles and Practice of Constraint Programming, pp.360-367, 2010.
DOI : 10.1007/978-3-642-15396-9_30

W. John, P. C. Mccormick, and . Chapin, Building High Integrity Applications with SPARK, 2015.

A. Miné, Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, 13th European Symposium on Programming, pp.3-17, 2004.
DOI : 10.1007/978-3-540-24725-8_2

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

P. Rümmer and T. Wahl, An SMT-LIB theory of binary floating-point arithmetic, Informal proceedings of 8th International Workshop on Satisfiability Modulo Theories (SMT) at FLoC, 2010.

M. David and . Russinoff, A mechanically checked proof of IEEE compliance of the floating point multiplication , division and square root algorithms of the AMD-K7 processor, LMS Journal of Computation and Mathematics, vol.1, pp.148-200, 1998.