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

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

S. Boldo, Deductive Formal Verification: How To Make Your Floating-Point Programs Behave, Thèse d'habilitation, 2014.
URL : https://hal.archives-ouvertes.fr/tel-01089643

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, Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd, IEEE Transactions on Computers, vol.57, issue.4, pp.462-471, 2008.
DOI : 10.1109/TC.2007.70819
URL : https://hal.archives-ouvertes.fr/inria-00080427

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

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.

S. Conchon, E. Contejean, and M. Iguernelala, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation, Logical Methods in Computer Science, vol.8, issue.3, pp.1-29, 2012.
DOI : 10.2168/LMCS-8(3:16)2012
URL : https://hal.archives-ouvertes.fr/hal-00798082

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

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

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

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

P. H. Sterbenz, Floating point computation, 1974.