. Frama-c, Framework for modular analyses of C

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

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

J. Filliâtre, The Why verification tool, 2002.

J. Filliâtre and C. Marché, Multi-prover Verification of C Programs, 6th International Conference on Formal Engineering Methods, pp.15-29, 2004.
DOI : 10.1007/978-3-540-30482-1_10

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

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

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon, The Objective Caml system release 3.01, Documentation and user's manual, 2001.

L. T. , M. Daumas, and L. Rideau, A generic library for floating-point numbers and its application to exact computing. TPHOLs, 2001.
URL : https://hal.archives-ouvertes.fr/hal-00157285

C. Marché, Jessie, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.1-2, 2007.
DOI : 10.1145/1292597.1292598

G. Melquiond and . Gappa, Automatic proof generation of arithmetic properties

G. Melquiond, Interval package for coq, http://www.msr-inria. inria.fr/ ~ gmelquio/soft/coq-interval

G. Melquiond, Floating-point arithmetic in the Coq system, Proceedings of the 8th Conference on Real Numbers and Computers, pp.93-102, 2008.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913

M. Yannick, Jessie plugin tutorial, 2008.

M. Yannick, Automatic Modular Static Safety Checking for C Programs, 2009.