A. Ayad and C. Marché, Multi-Prover Verification of Floating-Point Programs, In: Int. Joint Conference on Automated Reasoning. LNAI, vol.6173, pp.127-141, 2010.
DOI : 10.1007/978-3-642-14203-1_11

URL : https://hal.archives-ouvertes.fr/inria-00534333

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

S. Boldo, F. Clément, J. C. 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. 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 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

M. Brain, V. D-'silva, A. Griggio, L. Haller, and D. Kroening, Deciding floating-point logic with abstract conflict driven clause learning, Formal Methods in System Design, vol.48, issue.5, pp.213-245, 2014.
DOI : 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, Int. 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, pp.17-26, 2014.
DOI : 10.1007/978-3-319-08970-6_2

Z. Chihani, B. Marre, F. Bobot, and S. Bardin, Sharpening Constraint Programming Approaches for Bit-Vector Theory, p.CPAIOR, 2017.
DOI : 10.1109/DATE.2001.915055

S. Conchon, M. Iguernlala, K. Ji, G. Melquiond, and C. Fumex, A three-tier strategy for reasoning about floating-point numbers in SMT, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01522770

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-C, Int. Conf. on Software Engineering and Formal Methods, 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, 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

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

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

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

C. Fumex, C. Marché, and Y. Moy, Automated verification of floating-point computations in Ada programs, Inria, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01511183

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, 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, vol.16, issue.3, pp.271-305, 2000.
DOI : 10.1007/BFb0000475

J. Harrison, Formal Verification of Floating Point Trigonometric Functions, LNCS, vol.1954, pp.217-233, 2000.
DOI : 10.1007/3-540-40922-X_14

J. Harrison, Floating-point verification, Int. Symp. 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, Int. Symp. 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. R. Leino and M. Moskal, Usable auto-active verification, 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, Principles and Practice of Constraint Programming, pp.360-367, 2010.
DOI : 10.1007/978-3-642-15396-9_30

J. W. Mccormick and P. C. Chapin, Building High Integrity Applications with SPARK, 2015.
DOI : 10.1017/CBO9781139629294

A. Miné, Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors, 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

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, LNCS, vol.4963, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

P. Rümmer and T. Wahl, An SMT-LIB theory of binary floating-point arithmetic, In: Int. Workshop on Satisfiability Modulo Theories, 2010.

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