A. Ayad and C. Marché, Multi-prover verication of oating-point programs, Fifth IJCAR, LNAI, 2010.

M. Barnett and K. R. Leino, Weakest-precondition of unstructured programs, 6th PASTE, 2005.

M. Barnett, K. R. Leino, and W. Schulte, The Spec# Programming System: An Overview, CASSIS'04, p.4969, 2004.
DOI : 10.1007/978-3-540-30569-9_3

G. Barthe, T. Rezk, and A. Saabas, Proof Obligations Preserving Compilation, FAST'05, p.112126, 2005.
DOI : 10.1007/11679219_9

S. Boldo and J. Filliâtre, Formal Verication of Floating-Point Programs, 18th ARITH, p.187194, 2007.

S. Boldo and T. M. Nguyen, Hardware-independent proofs of numerical programs, 2nd NASA Formal Methods Symposium, p.1423, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00534410

S. Boldo and T. M. Nguyen, Proofs of numerical programs when the compiler optimizes, Innovations in Systems and Software Engineering, p.151160, 2011.
DOI : 10.1007/s11334-011-0151-6

URL : https://hal.archives-ouvertes.fr/hal-00777639

R. S. Boyer and Y. Yu, Automated correctness proofs of machine code programs for a commercial microprocessor, CADE, p.416430, 1992.
DOI : 10.1007/3-540-55602-8_181

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, 2003.
DOI : 10.1007/s10009-004-0167-4

L. Burdy and M. Pavlova, Java bytecode specication and verication, ACM symposium on Applied computing, 2006.

V. A. Carreño and P. S. Miner, Specication of the IEEE-854 oating-point standard in HOL and PVS, HOL'95, 1995.

C. Colby, P. Lee, G. Necula, F. Blau, M. Plesko et al., A certifying compiler for Java, ACM Conference PLDI, 2000.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRE?? Analyzer, ESOP, number 3444 in LNCS, p.2130, 2005.
DOI : 10.1007/978-3-540-31987-0_3

P. Cuoq and V. Prevosto, Value Plugin Documentation, Carbon version. CEA-List, 2011.

L. De-moura and N. Bjørner, Z3, an ecient SMT solver

D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal et al., Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software, FMICS, p.5369, 2009.
DOI : 10.1007/978-3-642-04570-7_6

G. Dowek and C. .. Muñoz, Conict detection and resolution for 1, 7th AIAA Aviation, Technology, Integration, and Operations Conference, 2007.

J. Filliâtre, Formal Verication of MIX Programs, 2007.

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus platform for deductive program verication, CAV, p.173177, 2007.

J. Harrison, Formal verication of oating point trigonometric functions, 3rd FMCAD, p.217233, 2000.

G. T. Leavens, Not a number of oating point problems, Journal of Object Technology, vol.5, issue.2, p.7583, 2006.

G. Melquiond, Proving Bounds on Real-Valued Functions with Computations, 4th IJCAR, p.217, 2008.
DOI : 10.1007/978-3-540-71070-7_2

URL : https://hal.archives-ouvertes.fr/hal-00180138

D. Monniaux, The pitfalls of verifying oating-point computations, Transactions on Programming Languages and Systems, vol.30, issue.3, p.12, 2008.

Y. Moy and C. Marché, Jessie Plugin Tutorial, Beryllium version. INRIA, 2009.

M. O. Myreen, Formal verication of machine-code programs, 2008.

T. M. Nguyen and C. Marché, Proving oating-point numerical programs by analysis of their assembly code, Research Report, vol.7655, 2011.

D. M. Russino, A mechanically checked proof of IEEE compliance of the oating point multiplication, division and square root algorithms of the AMD-K7 processor, LMS Journal of Computation and Mathematics, vol.1, p.148200, 1998.