A. Ayad and C. Marché, Multi-Prover Verification of Floating-Point Programs, Fifth International Joint Conference on Automated Reasoning, 2010.
DOI : 10.1007/978-3-642-14203-1_11

URL : https://hal.archives-ouvertes.fr/inria-00534333

M. Barnett and K. R. Leino, Weakest-precondition of unstructured programs, Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, PASTE '05, pp.82-87, 2005.

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, version 1, 2009.

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, pp.14-23, 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, pp.151-160, 2011.
DOI : 10.1007/s11334-011-0151-6

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

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 specification and verification, Proceedings of the 2006 ACM symposium on Applied computing , SAC '06, 2006.
DOI : 10.1145/1141277.1141708

V. A. 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.

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

I. Corporation, Intel 64 and IA-32 Architectures Software Developer's Manual. Manual, Intel, 2011.

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné et al., The ASTRE?? Analyzer, ESOP, number 3444 in Lecture Notes in Computer Science, pp.21-30, 2005.
DOI : 10.1007/978-3-540-31987-0_3

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

G. Dowek and C. .. Muñoz, Conflict detection and resolution for 1, Proceedings of the 7th AIAA Aviation, Technology, Integration, and Operations Conference, pp.2007-7737, 2007.

D. Elsner and J. , Fenlason, and friends. Using as, 2009.

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

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

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

T. Hubert, Analyse Statique et preuve de Programmes Industriels Critiques, Thèse de doctorat, 2008.

G. T. 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

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

S. P. Dandamudi, Guide to Assembly Language Programming in Linux. Spinger, 2005.

D. M. Russinoff, Abstract, LMS Journal of Computation and Mathematics, vol.11, pp.148-200, 1998.
DOI : 10.1112/S1461157000000176