, Assisted verification of elementary functions using Gappa, Proceedings of the 2006 ACM symposium on Applied computing , SAC '06, pp.1318-1322, 2006.
DOI : 10.1145/1141277.1141584
, Introduction to Approximation Theory, 1966.
, Handbook of Floating-Point Arithmetic, 2009.
DOI : 10.1007/978-0-8176-4705-6
URL : https://hal.archives-ouvertes.fr/ensl-00379167
, Users' manual for the Sollya tool, Release 2.0, https, 2010.
, The MPFI library
URL : https://hal.archives-ouvertes.fr/inria-00100985
, Numerical recipes: the art of scientific computing, Analytica Chimica Acta, vol.199, 1992.
DOI : 10.1016/S0003-2670(00)82860-3
, Méthodes d'optimisation globale basées sur l'analyse d'intervalle pour la résolution deprobì emes avec contraintes, 1997.
, Rigorous Global Search: Continuous Problems, 1996.
DOI : 10.1007/978-1-4757-2495-0
, AN OVERVIEW OF GLOBAL OPTIMIZATION USING INTERVAL ANALYSIS, 1992.
DOI : 10.1016/B978-0-12-505630-4.50021-3
, Taylor forms ? use and limits, Reliable Computing, vol.9, issue.1, pp.43-79, 2003.
DOI : 10.1023/A:1023061927787
, A Certified Infinite Norm for the Implementation of Elementary Functions, Seventh International Conference on Quality Software (QSIC 2007), pp.153-160, 2007.
DOI : 10.1109/QSIC.2007.4385491
URL : https://hal.archives-ouvertes.fr/ensl-00119810
, Floating point verification in HOL light: The exponential function, 1997.
DOI : 10.1007/BFb0000475
, Taylor models and other validated functional inclusion methods, International Journal of Pure and Applied Mathematics, vol.4, issue.4, pp.379-456, 2003.
, Certified and Fast Computation of Supremum Norms of Approximation Errors, 2009 19th IEEE Symposium on Computer Arithmetic, pp.169-176, 2009.
DOI : 10.1109/ARITH.2009.18
URL : https://hal.archives-ouvertes.fr/ensl-00334545
, Sichere und genaue Abschätzung des Approximationsfehlers bei rationalen Approximationen, 1996.
, Verifying Nonlinear Real Formulas Via Sums of Squares, Proc. of the 20th International Conference on Theorem Proving in Higher Order Logics, pp.102-118, 2007.
DOI : 10.1007/978-3-540-74591-4_9
, Methods and Applications of Interval Analysis, 1979.
DOI : 10.1137/1.9781611970906
, COSY INFINITY Version 9
, Rigorous global search using taylor models, Proceedings of the 2009 conference on Symbolic numeric computation, SNC '09, pp.11-20, 2009.
DOI : 10.1145/1577190.1577198
, Long-term stability of the Tevatron by verified global optimization, Nuclear Instruments and Methods in Physics Research Section A: Accelerators , Spectrometers, Detectors and Associated Equipment, proceedings of the 8th International Computational Accelerator Physics Conference -ICAP, pp.1-10, 2004.
, Efficient isolation of polynomial's real roots, Journal of Computational and Applied Mathematics, vol.162, issue.1, pp.33-50, 2004.
DOI : 10.1016/j.cam.2003.08.015
, TADIFF, a Flexible C++ Package for Automatic Differentiation Using Taylor Series, 1997.
, Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation , no. 19 in Frontiers in Appl, Math., SIAM, 2000.
DOI : 10.1137/1.9780898717761
, O((n log n)3/2) ALGORITHMS FOR COMPOSITION AND REVERSION OF POWER SERIES, Analytic Computational Complexity, pp.217-225, 1975.
DOI : 10.1016/B978-0-12-697560-4.50018-6
, Fast Algorithms for Manipulating Formal Power Series, Journal of the ACM, vol.25, issue.4, pp.581-595, 1978.
DOI : 10.1145/322092.322099
, Complex analysis. An introduction to the theory of analytic functions of one complex variable, 1979.
, ACETAF, ACM Transactions on Mathematical Software, vol.29, issue.3, pp.263-286, 2003.
DOI : 10.1145/838250.838252
, Effective bounds for P-recursive sequences, Journal of Symbolic Computation, vol.45, issue.10, p.arXiv, 2009.
DOI : 10.1016/j.jsc.2010.06.024
URL : https://hal.archives-ouvertes.fr/inria-00376219
, Rigorous analysis of nonlinear motion in particle accelerators, 1998.
, Global optimization in type theory, Ecole Polytechnique, 2008.
, Divider Circuit Verification with Model Checking and Theorem Proving, Theorem Proving in Higher Order Logics: 13th International Conference, pp.338-355, 2000.
DOI : 10.1007/3-540-44659-1_21
, Formal Verification of Floating Point Trigonometric Functions, Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000, pp.217-233, 2000.
DOI : 10.1007/3-540-40922-X_14
, Efficiency in a fully-expansive theorem prover, 1994.
, Program result checking: A new approach to making programs more reliable, Automata, Languages and Programming, 20th International Colloquium, ICALP93, Proceedings, pp.1-14, 1993.
DOI : 10.1007/3-540-56939-1_57
, Checking geometric programs or verification of geometric structures, Proceedings of the 12th Annual Symposium on Computational Geometry (FCRC'96), pp.159-165, 1996.
, Formal Global Optimization with Taylor Models, Proc. of the 4th International Joint Conference on Automated Reasoning, pp.408-422, 2008.
, A library of Taylor models for PVS automatic proof checker
, Schwankung von Polynomen zwischen Gitterpunkten, Mathematische Zeitschrift, vol.3, issue.1, pp.41-44, 1964.
DOI : 10.1007/BF01111276
, Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming, pp.96-293, 2003.
DOI : 10.1007/s10107-003-0387-5
, Combinatoire, algorithmique et géometrie des polynômes, 1996.
, Basic algorithms in real algebraic geometry and their complexity: from Sturm's theorem to the existential theory of reals, of Expositions in Mathematics, de Gruyter Lectures in Real Geometry, 1996.
DOI : 10.1515/9783110811117.1