Special functions, 1999. ,
Certain Rational Functions Whose Power Series Have Positive Coefficients, The American Mathematical Monthly, vol.79, issue.4, pp.327-341, 1972. ,
DOI : 10.2307/2978081
ACSL: ANSI/ISO C Specification Language, version 1, 2009. ,
Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Canonical Big Operators, 21st International Conference on Theorem Proving in Higher Order Logics, pp.86-101, 2008. ,
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193
Preuves formelles en arithmétiquesarithmétiquesà virgule flottante, 2004. ,
Floats and Ropes: A Case Study for Formal Numerical Program Verification, 36th International Colloquium on Automata, Languages and Programming, pp.91-102, 2009. ,
DOI : 10.1007/978-3-642-02930-1_8
Formal Proof of a Wave Equation Resolution Scheme: The Method Error, 1st Conference on Interactive Theorem Proving Conference, pp.147-162, 2010. ,
DOI : 10.1007/978-3-642-14052-5_12
URL : https://hal.archives-ouvertes.fr/inria-00450789
Annotated source code and Coq proofs, 2012. ,
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.200, issue.25???28, pp.423-456, 2013. ,
DOI : 10.1007/s10817-012-9255-4
URL : https://hal.archives-ouvertes.fr/hal-00649240
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
Combining Coq and Gappa for Certifying Floating-Point Programs, 16th Calculemus Symposium, pp.59-74, 2009. ,
DOI : 10.1109/TC.2008.200
URL : https://hal.archives-ouvertes.fr/inria-00432726
A formallyverified C compiler supporting floating-point arithmetic, Proceedings of the 21th IEEE Symposium on Computer Arithmetic, pp.107-115, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00743090
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives, Proceedings of the Second International Conference on Certified Programs and Proofs, number 7679 in LNCS, pp.289-304, 2012. ,
DOI : 10.1007/978-3-642-35308-6_22
URL : https://hal.archives-ouvertes.fr/hal-00712938
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011. ,
DOI : 10.1109/ARITH.2011.40
URL : https://hal.archives-ouvertes.fr/inria-00534854
CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Post-proceedings of the 5th International Workshop on Satisfiability Modulo Theories, pp.51-69, 2007. ,
DOI : 10.1016/j.entcs.2008.04.080
Inductively defined types, Colog'88, 1990. ,
DOI : 10.1007/3-540-52335-9_47
On the Partial Difference Equations of Mathematical Physics, IBM Journal of Research and Development, vol.11, issue.2, pp.215-234, 1967. ,
DOI : 10.1147/rd.112.0215
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
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Proceedings of the 14th International Conference on Theorem Proving in Higher-Order Logics (TPHOL'01), pp.169-184, 2001. ,
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285
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
Z3, an efficient SMT solver, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), pp.337-340, 2008. ,
Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975. ,
Adaptive Inexact Newton Methods with A Posteriori Stopping Criteria for Nonlinear Diffusion PDEs, SIAM Journal on Scientific Computing, vol.35, issue.4, pp.1761-1791, 2014. ,
DOI : 10.1137/120896918
URL : https://hal.archives-ouvertes.fr/hal-00681422
Sur le développement d'une fonction arbitraire suivant les fonctions de Laplace. Comptes-Rendus de l'Académie des Sciences, pp.224-227, 1908. ,
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
Positive Sums of the Classical Orthogonal Polynomials, SIAM Journal on Mathematical Analysis, vol.8, issue.3, pp.423-447, 1977. ,
DOI : 10.1137/0508032
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
Partial Differential Equations, 1986. ,
seL4, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010. ,
DOI : 10.1145/1743546.1743574
Recherches sur la courbe que forme une corde tendue mise en vibrations, Histoire de l'Académie Royale des Sciences et Belles Lettres, pp.214-249, 1747. ,
Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009. ,
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861
Jessie, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.1-2, 2007. ,
DOI : 10.1145/1292597.1292598
Formalisation et automatisation de preuves en analyses réelle et numérique, 2001. ,
Verification and Validation in Scientific Computing, 2010. ,
Finite Difference Schemes and Partial Differential Equations, 1989. ,