Multi-prover verification of floating-point programs, Fifth International Joint Conference on Automated Reasoning, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00534333
The spec# programming system: an overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS'04), Lecture Notes in Computer Science, vol.3362, pp.49-69, 2004. ,
Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Preuves formelles en arithmétiques à virgule flottante, 2004. ,
Pitfalls of a full floating-point proof: example on the formal proof of the Veltkamp/Dekker algorithms, Third International Joint Conference on Automated Reasoning, pp.52-66, 2006. ,
Floats & Ropes: a case study for formal numerical program verification, 36th International Colloquium on Automata, Languages and Programming, pp.91-102, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00432718
Kahan's algorithm for a correct discriminant computation at last formally proven, IEEE Trans. Comput, vol.58, issue.2, pp.220-225, 2009. ,
Formal proof of a wave equation resolution scheme: the method error, Proceedings of the First Interactive Theorem Proving Conference, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00450789
Proof and certification for an accurate discriminant, 12th IMACS-GAMM International Symposium on Scientific Computing, 2006. ,
Formal verification of floating-point programs, 18th IEEE International Symposium on Computer Arithmetic, pp.187-194, 2007. ,
URL : https://hal.archives-ouvertes.fr/hal-01174892
Combining Coq and Gappa for certifying floating-point programs, 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, pp.59-74, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00432726
Hardware-independent proofs of numerical programs, Proceedings of the Second NASA Formal Methods Symposium. number NASA/CP-2010-216215 in NASA Conference Publication, pp.14-23, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00534410
Proofs of numerical programs when the compiler optimizes, Innov. Syst. Softw. Eng, vol.7, pp.1-10, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00777639
An overview of JML tools and applications, Int. J. Softw. Tools Technol. Transf. (STTT), vol.7, issue.3, pp.212-232, 2005. ,
SPARK?an annotated Ada subset for safety-critical programming, Proceedings of the Conference on TRI-ADA'90, TRI-Ada'90, pp.392-402, 1990. ,
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. ,
The ASTRÉE analyzer, In: ESOP. Lecture Notes in Computer Science, vol.3444, pp.21-30, 2005. ,
A generic library of floating-point numbers and its application to exact computing, 14th International Conference on Theorem Proving in Higher Order Logics, pp.169-184, 2001. ,
A floating point technique for extending the available precision, Numerische Mathematik, vol.18, issue.3, pp.224-242, 1971. ,
Towards an industrial use of FLUCTUAT on safety-critical avionics software, FMICS, LNCS, pp.53-69, 2009. ,
The Why/Krakatoa/Caduceus platform for deductive program verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007. ,
An experience report on the verification of algorithms in the c++ standard library using frama-c, Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, pp.191-204, 2010. ,
Static analysis of numerical algorithms, ) SAS. LNCS, pp.18-34, 2006. ,
Formal verification of floating point trigonometric functions, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, pp.217-233, 2000. ,
Accuracy and stability of numerical algorithms, 2002. ,
On the cost of Floating-Point Computation Without Extra-Precise Arithmetic. World-Wide Web document, 2004. ,
Not a number of floating point problems, J. Object Technol, vol.5, issue.2, pp.75-83, 2006. ,
Floating-point arithmetic in the Coq system, Proceedings of the 8th Conference on Real Numbers and Computers, pp.93-102, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00797913
Proving bounds on real-valued functions with computations, Proceedings of the 4th International Joint Conference on Automated Reasoning, pp.2-17, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00180138
Analyse statique : de la théorie à la pratique. Habilitation to direct research Université Joseph Fourier, 2009. ,
Jessie Plugin Tutorial, Beryllium version, INRIA, 2009. ,
Modular inference of subprogram contracts for safety checking, J. Symb. Comput, vol.45, pp.1184-1211, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00534331
Cil: Intermediate language and tools for analysis and transformation of c programs, Conference on Compiler Construction (CC'02), 2002. ,
A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor, LMS J. Comput. Math, vol.1, pp.148-200, 1998. ,
Floating Point Computation, Upper Saddle River, 1974. ,
Algolprocedures voor het berekenen van een inwendig product in dubbele precisie, RC-Informatie Technische Hogeschool Eindhoven, vol.22, 1968. ,
Rounding Errors in Algebraic Processes, 1963. ,