F. Bobot, S. Conchon, E. Contejean, M. Iguernelala, S. Lescuyer et al., The Alt-Ergo automated theorem prover, 2008.

S. Conchon, SMT techniques and their applications: from Alt-Ergo to Cubicle , Thèse d'habilitation, 2012.

C. Barrett and C. Tinelli, CVC3, 19th International Conference on Computer Aided Verification, pp.298-302, 2007.
DOI : 10.1007/978-3-540-73368-3_34

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

G. Melquiond, Proving Bounds on Real-Valued Functions with Computations, Proceedings of the 4th International Joint Conference on Automated Reasoning, pp.2-17, 2008.
DOI : 10.1007/978-3-540-71070-7_2

URL : https://hal.archives-ouvertes.fr/hal-00180138

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

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

Y. Moy and C. Marché, The Jessie plugin for Deduction Verification in Frama-C ? Tutorial and Reference Manual, INRIA & LRI, 2011.

Y. Moy and C. Marché, Modular inference of subprogram contracts for safety checking, Journal of Symbolic Computation, vol.45, issue.11, pp.1184-1211, 2010.
DOI : 10.1016/j.jsc.2010.06.004

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

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.

J. Kuipers, Quaternions and Rotation Sequences: A Primer With Applications to Orbits, Aerospace, and Virtual Reality, 1999.
DOI : 10.7546/giq-1-2000-127-143

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

J. Filliâtre, A. Paskevich, and A. Stump, The 2nd verified software competition: Experience report, COM- PARE2012: 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, 2012.

V. Klebanov, P. Müller, N. Shankar, G. T. Leavens, V. Wüstholz et al., The 1st Verified Software Competition: Experience Report, FM, pp.154-168, 2011.
DOI : 10.1007/978-3-540-71067-7_6

D. R. Cok, J. R. Kiniry, and . Esc, Java2 implementation notes, Tech. rep., http://secure.ucd.ie/products/opensource, 2007.

C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. C. Rinard, Using First-Order Theorem Provers in the Jahob Data Structure Verification System, 8th International Conference on Verification, Model Checking, and Abstract Interpretation, pp.74-88, 2007.
DOI : 10.1007/978-3-540-69738-1_5

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

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, Theorem Proving in Higher Order Logics (TPHOLs), 2009.
DOI : 10.1007/978-3-540-74591-4_15

M. Barnett, K. R. Leino, and W. Schulte, The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS'04), pp.49-69, 2004.
DOI : 10.1007/978-3-540-30569-9_3

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

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

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

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

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

S. Boldo and T. M. Nguyen, Hardware-independent proofs of numerical programs, Proceedings of the Second NASA Formal Methods Symposium, 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, Innovations in Systems and Software Engineering, vol.1, issue.3, pp.151-160, 2011.
DOI : 10.1007/s11334-011-0151-6

URL : https://hal.archives-ouvertes.fr/hal-00777639

T. M. Nguyen and C. Marché, Hardware-Dependent Proofs of Numerical Programs, Certified Programs and Proofs, pp.314-329, 2011.
DOI : 10.1112/S1461157000000176

URL : https://hal.archives-ouvertes.fr/hal-00772508

T. M. Nguyen, Taking architecture and compiler into account in formal proofs of numerical programs, Thèse de doctorat, 2012.
URL : https://hal.archives-ouvertes.fr/tel-00710193

G. Melquiond, Floating-point arithmetic in the Coq system, Information and Computation, vol.216, pp.14-23, 2012.
DOI : 10.1016/j.ic.2011.09.005

URL : https://hal.archives-ouvertes.fr/hal-00797913

B. Akbarpour and L. C. Paulson, MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions, Journal of Automated Reasoning, vol.7, issue.4, pp.175-205, 2010.
DOI : 10.1007/s10817-009-9149-2

T. Hubert and C. Marché, Separation analysis for deductive verification, in: Heap Analysis and Verification (HAV'07), pp.81-93, 2007.

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.

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

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

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

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

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

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, vol.5825, pp.53-69, 2009.
DOI : 10.1007/978-3-642-04570-7_6

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

G. Dowek and C. .. Muñoz, Conflict detection and resolution for 1, Proceedings of the 7th AIAA Aviation, Technology, Integration, and Operations Conference, pp.2007-7737, 2007.

S. Blazy and X. Leroy, Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning, vol.29, issue.6, pp.263-288, 2009.
DOI : 10.1007/s10817-009-9148-3

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

P. Herms, Certification of a tool chain for deductive program verification, Thèse de doctorat, 2013.
URL : https://hal.archives-ouvertes.fr/tel-00789543