W. Kahan, Miscalculating Area and Angles of a Needle-like Triangle Unpublished manuscript, 1986.

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

S. Boldo, How to Compute the Area of a Triangle: A Formal Revisit, 2013 IEEE 21st Symposium on Computer Arithmetic, pp.91-98, 2013.
DOI : 10.1109/ARITH.2013.29
URL : https://hal.archives-ouvertes.fr/hal-00862653

V. A. Carreñocarre?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

W. Kahan, On the Cost of Floating-Point Computation Without Extra-Precise Arithmetic, 2004.

S. Boldo, Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven, IEEE Transactions on Computers, vol.58, issue.2, pp.220-225, 2009.
DOI : 10.1109/TC.2008.200

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

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

G. Melquiond, Proving Bounds on Real-Valued Functions with Computations, Proceedings of the 4th international joint conference on Automated Reasoning, ser. IJCAR '08, pp.2-17, 2008.
DOI : 10.1007/978-3-540-71070-7_2
URL : https://hal.archives-ouvertes.fr/hal-00180138

. Microprocessor-standards-committee, IEEE Standard for Floating-Point Arithmetic, IEEE Std, pp.754-2008, 2008.

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

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, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

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