A. Ayad and C. Marché, Multi-Prover Verification of Floating-Point Programs, IJCAR 5, pp.127-141, 2010.
DOI : 10.1007/978-3-642-14203-1_11
URL : https://hal.archives-ouvertes.fr/inria-00534333

F. Bobot, S. Conchon, E. Contejean, M. Iguernelala, A. Mahboubi et al., A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic, IJCAR 6, 2012.
DOI : 10.1007/978-3-642-31365-3_8
URL : https://hal.archives-ouvertes.fr/hal-00687640

S. Conchon and E. Contejean, Alt-Ergo, 2006.
URL : https://hal.archives-ouvertes.fr/hal-01093000

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

F. De-dinechin, C. Lauter, and G. Melquiond, Certifying the Floating-Point Implementation of an Elementary Function Using Gappa, IEEE Transactions on Computers, vol.60, issue.2, pp.242-253, 2011.
DOI : 10.1109/TC.2010.128
URL : https://hal.archives-ouvertes.fr/ensl-00200830

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

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

S. Gao, M. K. Ganai, F. Ivancic, A. Gupta, S. Sankaranarayanan et al., Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems, FMCAD, pp.81-89, 2010.

F. Ivancic, M. K. Ganai, S. Sankaranarayanan, and A. Gupta, Numerical stability analysis of floating-point computations using software model checking, Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), pp.49-58, 2010.
DOI : 10.1109/MEMCOD.2010.5558622

J. Muller, N. Brisebarre, F. De-dinechin, C. Jeannerod, V. Lefèvre et al., Handbook of Floating-Point Arithmetic, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01766584

P. Rümmer and T. Wahl, An SMT-LIB theory of binary floating-point arithmetic, SMT 8 at FLoC, 2010.