A. Ayad and C. Marché, Behavioral properties of floating-point programs. Hisseo publications, 2009.

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

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

B. Beckert, R. Hähnle, and P. H. Schmitt, Verification of Object-Oriented Software: The KeY Approach, LNCS, vol.4334, 2007.
DOI : 10.1007/978-3-540-69061-0

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 and T. M. Nguyen, Hardware-independent proofs of numerical programs, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00534410

A. Brillout, D. Kroening, and T. Wahl, Mixed abstractions for floating-point arithmetic, 2009 Formal Methods in Computer-Aided Design, pp.69-76, 2009.
DOI : 10.1109/FMCAD.2009.5351141

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry et al., An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer, vol.box, issue.3, 2004.
DOI : 10.1007/s10009-004-0167-4

P. Chalin, Reassessing JML's logical foundation, Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP'05), 2005.

D. R. Cok, J. R. Kiniry, and . Esc, Java2 implementation notes, 2007.

S. Conchon, E. Contejean, J. Kanig, and S. Lescuyer, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Proceedings of the 5th International Workshop SMT, pp.51-69, 2007.
DOI : 10.1016/j.entcs.2008.04.080

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Theorem Proving in Higher Order Logics (TPHOLs'01), volume 2152 of LNCS, p.169, 2001.
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285

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

B. Dutertre and L. De-moura, The Yices SMT solver, 2006.

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, 19th International Conference CAV'2007, 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

J. Harrison, Floating point verification in HOL Light: The exponential function. Formal Methods in System Design, pp.271-305, 2000.

G. Leavens, Not a Number of Floating Point Problems., The Journal of Object Technology, vol.5, issue.2, pp.75-83, 2006.
DOI : 10.5381/jot.2006.5.2.c8

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

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

P. S. Miner, Defining the IEEE-854 floating-point standard in PVS, 1995.

D. Monniaux, The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems, vol.30, issue.3, p.12, 2008.
DOI : 10.1145/1353445.1353446
URL : https://hal.archives-ouvertes.fr/hal-00128124

D. Monniaux, Automatic modular abstractions for linear constraints, 36th ACM Symposium POPL 2009, pp.140-151, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00336144

J. S. Moore, T. Lynch, and M. Kaufmann, A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program, IEEE Transactions on Computers, vol.47, issue.9, pp.913-926, 1998.
DOI : 10.1109/12.713311

E. Reeber and J. Sawada, Combining ACL2 and an automated verification tool to verify a multiplier, Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications , ACL2 '06, pp.63-70, 2006.
DOI : 10.1145/1217975.1217990

W. Schulte, S. Xia, J. Smans, and F. Piessens, A glimpse of a verifying C compiler

K. Zee, V. Kuncak, and M. Rinard, Full functional verification of linked data structures, PLDI'08, pp.349-361, 2008.