Elamur Research⌕
☰
home / papers / 2010 / Verification methods: rigorous results using floating-point arithmetic

Verification methods: rigorous results using floating-point arithmetic

Paper · 2010 · Siegfried M. Rump

Summary

Ordinary floating-point computations give approximate answers with no guarantee of accuracy. Verification methods address this by producing mathematically rigorous bounds, for example proving that a true solution exists inside a computed enclosure. This survey by Rump explains how such methods are built and where they break down. It has three parts of similar size. Part 1 covers the basic tools: floating-point arithmetic, error-free transformations, directed rounding and interval arithmetic, along with historical remarks. Part 2 treats finite-dimensional problems such as dense and sparse linear systems, nonlinear equations, polynomial roots, eigenvalue bounds, quadrature, automatic differentiation and optimization. Part 3 handles infinite-dimensional problems, namely boundary value problems for differential equations. A recurring theme is that interval arithmetic earned a poor reputation through misuse, and that rigorous algorithms need different design principles from conventional numerical ones. Many algorithms are given as runnable MATLAB/INTLAB code, so readers can test them directly.

Key points

  • Published in Acta Numerica 19 (2010), pp. 287–449. The section on semilinear elliptic boundary value problems was written by Michael Plum (Karlsruhe).
  • A probabilistic argument shows that interval Gaussian elimination (IGA) fails even for small, well-conditioned random matrices.
  • Topics include M-matrices, simple and multiple roots and eigenvalues (including clusters), semidefinite programming, and enclosures of gradients, Hessians, Taylor coefficients and slopes.
  • Global optimization is covered only briefly, with readers referred to Neumaier's 2004 Acta Numerica survey.
  • In 2004, Bornemann, Laurie, Wagon and Waldvogel relied on INTLAB, the MATLAB toolbox for reliable computing, to solve half of Trefethen's SIAM 10 × 10-digit challenge problems.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Hamburg University of TechnologyHamburg · Germany3 works · 2,676 citations🎓Waseda UniversityTokyo · Japan22 works · 869 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksMathematics · 233 worksComputational Theory and Mathematics · 496 worksModeling and Simulation · 12 works

Cite

Cite as Siegfried M. Rump. 2010. Verification methods: rigorous results using floating-point arithmetic. Acta Numerica 19:287–449.

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{rump2010verification,
  title = {{Verification methods: rigorous results using floating-point arithmetic}},
  author = {Siegfried M. Rump},
  booktitle = {Acta Numerica 19:287–449},
  year = {2010},
  doi = {10.1017/s096249291000005x},
  url = {https://doi.org/10.1017/s096249291000005x}
}

References

225 references, 3 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. J. P. Abbott and R. P. Brent (1975), ‘Fast local convergence with single and multistep methods for nonlinear equations’, Austr. Math. Soc. B 19, 173–199. find
  2. ACRITH (1984), IBM High-Accuracy Arithmetic Subroutine Library (ACRITH), Release 1, IBM Deutschland GmbH, Böblingen. find
  3. R. A. Adams (1975), Sobolev Spaces, Academic Press, New York. find
  4. G. Alefeld (1994), Inclusion methods for systems of nonlinear equations. In Topics in Validated Computations (J. Herzberger, ed.), Studies in Computational Mathematics, Elsevier, Amsterdam, pp. 7–26. find
  5. G. Alefeld and J. Herzberger (1974), Einführung in die Intervallrechnung, BI Wis-senschaftsverlag. find
  6. G. Alefeld, V. Kreinovich and G. Mayer (1997), ‘On the shape of the symmetric, persymmetric, and skew-symmetric solution set’, SIAM J. Matrix Anal. Appl. 18, 693–705. find
  7. G. Alefeld, V. Kreinovich and G. Mayer (2003), ‘On the solution sets of particular classes of linear interval systems’, J. Comput. Appl. Math. 152, 1–15. find
  8. E. Anderson, Z. Bai, C. Bischof, J. Demmel, J. Dongarra, J. Du Croz, A. Greenbaum, S. Hammarling, A. McKenney, S. Ostrouchov and D. C. Sorensen (1995), LAPACK User’s Guide, Release 2.0, 2nd edn, SIAM, Philadelphia. find
  9. M. V. A. Andrade, J. L. D. Comba and J. Stolfi (1994), Affine arithmetic. Extended abstract, presented at INTERVAL’94 , St. Petersburg. find
  10. ARITHMOS (1986), ARITHMOS: Benutzerhandbuch, Siemens AG, Bibl.-Nr. U 2900-I-Z87-1 edition. find
  11. M. Aschbacher (1994), Sporadic Groups, Cambridge University Press. find
  12. A. Avizienis (1961), ‘Signed-digit number representations for fast parallel arithmetic’, Ire Trans. Electron. Comp. EC-10, 389–400. find
  13. H. Bauer (1978), Wahrscheinlichkeitstheorie und Grundzüge der Maßtheorie, 3rd edn, de Gruyter, Berlin. find
  14. O. Beaumont (2000), Solving interval linear systems with oblique boxes. Research report PI 1315, INRIA. find
  15. H. Behnke (1989), Die Bestimmung von Eigenwertschranken mit Hilfe von Vari-ationsmethoden und Intervallarithmetik. Dissertation, Institut für Mathematik, TU Clausthal. find
  16. H. Behnke and F. Goerisch (1994), Inclusions for eigenvalues of selfadjoint problems. In Topics in Validated Computations (J. Herzberger, ed.), Studies in Computational Mathematics, Elsevier, Amsterdam, pp. 277–322. find
  17. A. Ben-Tal and A. Nemirovskii (2001), Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, Philadelphia. find
  18. F. Bernelli Zazzera, M. Vasile, M. Massari and P. Di Lizia (2004), Assessing the accuracy of interval arithmetic estimates in space flight mechanics. Final report, Ariadna id: 04/4105, Contract Number: 18851/05/NL/MV. find
  19. Y. Bertot and P. Castéran (2004), Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, Springer. find
  20. M. Berz and K. Makino (1999), ‘New methods for high-dimensional verified quadrature’, Reliable Computing 5, 13–22. find
  21. C. H. Bischof, A. Carle, G. Corliss and A. Griewank (1991), ADIFOR: Generating derivative codes from Fortran programs. Technical report, Mathematics and Computer Science Division, Argonne National Laboratory. find
  22. B. Borchers (1999), ‘SDPLIB 1.2: A library of semidefinite programming test problems’, Optim. Methods Software 11, 683–690. find
  23. F. Bornemann, D. Laurie, S. Wagon and J. Waldvogel (2004), The SIAM 100-Digit Challenge: A Study in High-Accuracy Numerical Computing, SIAM, Philadelphia. find
  24. N. C. Börsken (1978), Komplexe Kreis-Standardfunktionen. Diplomarbeit, Frei-burger Intervall-Ber. 78/2, Institut für Angewandte Mathematik, Universität Freiburg. find
  25. K. D. Braune (1987), Hochgenaue Standardfunktionen für reelle und komplexe Punkte und Intervalle in beliebigen Gleitpunktrastern. Dissertation, Universität Karlsruhe. find
  26. B. Breuer, J. Horák, P. J. McKenna and M. Plum (2006), ‘A computer-assisted existence and multiplicity proof for travelling waves in a nonlinearly supported beam’, J. Diff. Equations 224, 60–97. find
  27. B. Breuer, P. J. McKenna and M. Plum (2003), ‘Multiple solutions for a semilinear boundary value problem: A computational multiplicity proof’, J. Diff. Equations 195, 243–269. find
  28. B. M. Brown, D. K. R. McCormack and A. Zettl (2000), ‘On a computer assisted proof of the existence of eigenvalues below the essential spectrum of the Sturm–Liouville problem’, J. Comput. Appl. Math. 125, 385–393. find
  29. M. W. Browne (1988), Is a math proof a proof if no one can check it? The New York Times, December 1988, p. 1. find
  30. J. R. Bunch, J. W. Demmel and C. F. Van Loan (1989), ‘The strong stability of algorithms for solving symmetric linear systems’, SIAM J. Matrix Anal. Appl. 10, 494–499. find
  31. F. Bünger (2008), private communication. find
  32. O. Caprani and K. Madsen (1978), ‘Iterative methods for interval inclusion of fixed points’, BIT Numer. Math. 18, 42–51. find
  33. F. Chatelin (1988), Analyse statistique de la qualité numérique et arithmétique de la résolution approchée d’équations par calcul sur ordinateur. Technical Report F.133, Centre Scientifique IBM–France. find
  34. Y. S. Choi and P. J. McKenna (1993), ‘A mountain pass method for the numerical solutions of semilinear elliptic problems’, Nonlinear Anal. Theory Methods Appl. 20, 417–437. find
  35. L. Collatz (1942), ‘Einschließungssatz für die charakteristischen Zahlen von Matrizen’, Math. Z. 48, 221–226. find
  36. G. F. Corliss and L. B. Rall (1987), ‘Adaptive, self-validating numerical quadrature’, SIAM J. Sci. Statist. Comput. 8, 831–847. find
  37. G. Corliss, C. Faure, A. Griewank, L. Hascoët and U. Nauman (2002), Automatic Differentiation of Algorithms: From Simulation to Optimization, Springer. find
  38. A. Cuyt, B. Verdonk, S. Becuwe and P. Kuterna (2001), ‘A remarkable example of catastrophic cancellation unraveled’, Computing 66, 309–320. find
  39. E. N. Dancer and S. S. Yan (2005), ‘On the superlinear Lazer–McKenna conjecture’, J. Diff. Equations 210, 317–351. find
  40. S. M. Rump Verification methods G. Darboux (1876), ‘Sur les développements en série des fonctions d’une seule variable’, J. des Mathématiques Pures et Appl. 3, 291–312. find
  41. M. Daumas, G. Melquiond and C. Muñoz (2005), Guaranteed proofs using interval arithmetic. In Proc. 17th IEEE Symposium on Computer Arithmetic (ARITH’05). find
  42. T. J. Dekker (1971), ‘A floating-point technique for extending the available precision’, Numer. Math. 18, 224–242. find
  43. J. B. Demmel (1989), On floating point errors in Cholesky. LAPACK Working Note 14 CS-89-87, Department of Computer Science, University of Tennessee, Knoxville, TN, USA. find
  44. J. B. Demmel, B. Diament and G. Malajovich (2001), ‘On the complexity of computing error bounds’, Found. Comput. Math. 1, 101–125. find
  45. J. B. Demmel, I. Dumitriu, O. Holtz and P. Koev (2008), Accurate and efficient expression evaluation and linear algebra. In Acta Numerica, Vol. 17, Cambridge University Press, pp. 87–145. find
  46. J. B. Demmel, Y. Hida, W. Kahan, X. S. Li, S. Mukherjee and E. J. Riedy (2004), Error bounds from extra precise iterative refinement. Report no. ucb/csd-04-1344, Computer Science Devision (EECS), University of California, Berkeley. find
  47. P. S. Dwyer (1951), Linear Computations, Wiley, New York/London. find
  48. C. Eckart and G. Young (1936), ‘The approximation of one matrix by another of lower rank’, Psychometrika 1, 211–218. find
  49. J.-P. Eckmann, H. Koch and P. Wittwer (1984), ‘A computer-assisted proof of universality for area-preserving maps’, Mem. Amer. Math. Soc. 47, 289. find
  50. P. Eijgenraam (1981), The solution of initial value problems using interval arithmetic. find
  51. B. Fazekas, M. Plum and C. Wieners (2005), Enclosure for biharmonic equation. In Dagstuhl Online Seminar Proceedings 05391. http://drops.dagstuhl.de/portal/05391/. ↗
  52. L. H. de Figueiredo and J. Stolfi (2004), ‘Affine arithmetic: Concepts and applications’, Numer. Algorithms 37, 147–158. find
  53. L. V. Foster (1994), ‘Gaussian elimination with partial pivoting can fail in practice’, SIAM J. Matrix Anal. Appl. 14, 1354–1362. find
  54. L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier and P. Zimmermann (2005), MPFR: A multiple-precision binary floating-point library with correct rounding. Research Report RR-5753, INRIA. Code and documentation available at: http://hal.inria.fr/inria-00000818. *) ↗
  55. A. Frommer (2001), Proving conjectures by use of interval arithmetic. In Perspectives on Enclosure Methods: SCAN 2000 (U. Kulisch et al., ed.), Springer. find
  56. Z. Galias and P. Zgliczynski (1998), ‘Computer assisted proof of chaos in the Lorenz equations’, Physica D 115, 165–188. find
  57. I. Gargantini and P. Henrici (1972), ‘Circular arithmetic and the determination of polynomial zeros’, Numer. Math. 18, 305–320. find
  58. B. Gidas, W. Ni and L. Nirenberg (1979), ‘Symmetry and related problems via the maximum principle’, Comm. Math. Phys. 68, 209–243. find
  59. D. Gilbarg and N. S. Trudinger (1983), Elliptic Partial Differential Equations of Second Order, 2nd edn, Springer. *) published in ACM Transaction on Mathematical Software (TOMS) 33, article 13, 2007 find
  60. D. Goldberg (1991), ‘What every computer scientist should know about floating-point arithmetic’, ACM Comput. Surv. 23, 5–48.
  61. M. J. C. Gordon (2000), From LCF to HOL: A short history. In Proof, Language, and Interaction: Essays in Honour of Robin Milner (G. Plotkin, C. Stirling and M. Tofte, eds), MIT Press. http://www.cl.cam.ac.uk/˜mjcg/papers/HolHistory.html. ↗
  62. D. Gorenstein, R. Lyons and R. Solomon (1994), The Classification of the Finite Simple Groups, Vol. 40 of Math. Surveys Monographs, AMS, Providence, RI. find
  63. A. Griewank (2003), A mathematical view of automatic differentiation. In Acta Numerica, Vol. 12, Cambridge University Press, pp. 321–398. find
  64. P. Grisvard (1985), Elliptic Problems in Nonsmooth Domains, Pitman, Boston. find
  65. E. Hansen (1969), The centered form. In Topics in Interval Analysis (E. Hansen, ed.), Oxford University Press, pp. 102–106. find
  66. E. R. Hansen and R. Smith (1967), ‘Interval arithmetic in matrix computations II’, SIAM J. Numer. Anal. 4, 1–9. find
  67. G. Hargreaves (2002), Interval analysis in MATLAB. Master’s thesis, University of Manchester. http://www.manchester.ac.uk/mims/eprints. ↗
  68. J. Hass, M. Hutchings and R. Schlafly (1995), ‘The double bubble conjecture’, Electron. Res. Announc. Amer. Math. Soc. 1, 98–102. find
  69. D. J. Higham and N. J. Higham (1992a), ‘Componentwise perturbation theory for linear systems with multiple right-hand sides’, Linear Algebra Appl. 174, 111–129. find
  70. D. J. Higham and N. J. Higham (1992b), ‘Backward error and condition of structured linear systems’, SIAM J. Matrix Anal. Appl. 13, 162–175. find
  71. N. J. Higham (2002), Accuracy and Stability of Numerical Algorithms, 2nd edn, SIAM, Philadelphia. find
  72. J. Hölzl (2009), Proving real-valued inequalities by computation in Isabelle/HOL. Diplomarbeit, Fakultät für Informatik der Technischen Universität München. find
  73. IEEE 754 (2008), ANSI/IEEE 754-2008: IEEE Standard for Floating-Point Arithmetic, New York. find
  74. C. Jansson (1991), ‘Interval linear systems with symmetric matrices, skew-symmetric matrices, and dependencies in the right hand side’, Computing 46, 265–274. find
  75. C. Jansson (1994), On self-validating methods for optimization problems. In Topics in Validated Computations (J. Herzberger, ed.), Studies in Computational Mathematics, Elsevier, Amsterdam, pp. 381–438. find
  76. C. Jansson (1997), ‘Calculation of exact bounds for the solution set of linear interval systems’, Linear Algebra Appl. 251, 321–340. find
  77. C. Jansson (2004a), ‘A rigorous lower bound for the optimal value of convex optimization problems’, J. Global Optim. 28, 121–137. find
  78. C. Jansson (2004b), ‘Rigorous lower and upper bounds in linear programming’, SIAM J. Optim. 14, 914–935. find
  79. C. Jansson (2006), VSDP: A MATLAB software package for verified semidefinite programming. In NOLTA 2006 , pp. 327–330. find
  80. C. Jansson (2009), ‘On verified numerical computations in convex programming’, Japan J. Indust. Appl. Math. 26, 337–363. find
  81. S. M. Rump Verification methods C. Jansson and J. Rohn (1999), ‘An algorithm for checking regularity of interval matrices’, SIAM J. Matrix Anal. Appl. 20, 756–776. find
  82. C. Jansson, D. Chaykin and C. Keil (2007), ‘Rigorous error bounds for the optimal value in semidefinite programming’, SIAM J. Numer. Anal. 46, 180–200. http://link.aip.org/link/?SNA/46/180/1. ↗
  83. W. M. Kahan (1968), A more complete interval arithmetic. Lecture notes for a summer course at the University of Michigan. find
  84. Y. Kanzawa and S. Oishi (1999a), ‘Imperfect singular solutions of nonlinear equations and a numerical method of proving their existence’, IEICE Trans. Fundamentals E82-A, 1062–1069. find
  85. Y. Kanzawa and S. Oishi (1999b), ‘Calculating bifurcation points with guaranteed accuracy’, IEICE Trans. Fundamentals E82-A, 1055–1061. find
  86. T. Kato (1966), Perturbation Theory for Linear Operators, Springer, New York. find
  87. R. B. Kearfott (1997), ‘Empirical evaluation of innovations in interval branch and bound algorithms for nonlinear systems’, SIAM J. Sci. Comput. 18, 574–594. find
  88. R. B. Kearfott, M. Dawande, K. Du and C. Hu (1992), ‘INTLIB: A portable Fortran-77 elementary function library’, Interval Comput. 3, 96–105. find
  89. R. B. Kearfott, J. Dian and A. Neumaier (2000), ‘Existence verification for singular zeros of complex nonlinear systems’, SIAM J. Numer. Anal. 38, 360–379. find
  90. R. B. Kearfott, M. T. Nakao, A. Neumaier, S. M. Rump, S. P. Shary and P. van Hentenfyck (2005) Standardized notation in interval analysis. In Proc. XIII Baikal International School–Seminar: Optimization Methods and their Applications, Vol. 4, Melentiev Energy Systems Institute SB RAS, Irkutsk. find
  91. C. Keil (2006), Lurupa: Rigorous error bounds in linear programming. In Algebraic and Numerical Algorithms and Computer-assisted Proofs (B. Buchberger, S. Oishi, M. Plum and S. M. Rump, eds), Vol. 05391 of Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum für Informati… find
  92. C. Keil and C. Jansson (2006), ‘Computational experience with rigorous error bounds for the Netlib linear programming library’, Reliable Computing 12, 303–321. http://www.optimization-online.org/DB HTML/2004/12/1018.html. ↗
  93. R. Klatte, U. Kulisch, A. Wiethoff, C. Lawo and M. Rauch (1993), C-XSC A C++ Class Library for Extended Scientific Computing, Springer, Berlin. find
  94. O. Knüppel (1994), ‘PROFIL/BIAS: A fast interval library’, Computing 53, 277– 287. find
  95. O. Knüppel (1998), PROFIL/BIAS and extensions, Version 2.0. Technical report, Institut für Informatik III, Technische Universität Hamburg–Harburg. find
  96. D. E. Knuth (1969), The Art of Computer Programming: Seminumerical Algorithms, Vol. 2, Addison-Wesley, Reading, MA. find
  97. L. V. Kolev and V. Mladenov (1997), Use of interval slopes in implementing an interval method for global nonlinear DC circuit analysis. Internat. J. Circuit Theory Appl. 12, 37–42. find
  98. W. Krämer (1987), Inverse Standardfunktionen für reelle und komplexe Intervall-argumente mit a priori Fehlerabschätzung für beliebige Datenformate. Dissertation, Universität Karlsruhe. find
  99. W. Krämer (1991), Verified solution of eigenvalue problems with sparse matrices. In Proc. 13th World Congress on Computation and Applied Mathematics, pp. 32–33. find
  100. R. Krawczyk (1969a), ‘Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken’, Computing 4, 187–201. find
  101. R. Krawczyk (1969b), ‘Fehlerabschätzung reeller Eigenwerte und Eigenvektoren von Matrizen’, Computing 4, 281–293. find
  102. R. Krawczyk and A. Neumaier (1985), ‘Interval slopes for rational functions and associated centered forms’, SIAM J. Numer. Anal. 22, 604–616. find
  103. V. Kreinovich, A. V. Lakeyev and S. I. Noskov (1993), ‘Optimal solution of interval linear systems is intractable (NP-hard)’, Interval Comput. 1, 6–14. find
  104. V. Kreinovich, A. Neumaier and G. Xiang (2008), ‘Towards a combination of interval and ellipsoid uncertainty’, Vych. Techn. (Computational Technologies) 13, 5–16. find
  105. U. Kulisch (1981), Computer Arithmetic in Theory and Practice, Academic Press. find
  106. M. La Porte and J. Vignes (1974), ‘Etude statistique des erreurs dans l’arith-métique des ordinateurs: Application au contrôle des résultats d’algorithmes númeriques’, Numer. Math. 23, 63–72. find
  107. O. A. Ladyzhenskaya and N. N. Uralt́seva (1968), Linear and Quasilinear Elliptic Equations, Academic Press, New York. find
  108. J. Lahmann and M. Plum (2004), ‘A computer-assisted instability proof for the Orr–Sommerfeld equation with Blasius profile’, Z. Angew. Math. Mech. 84, 188–204. find
  109. C. W. H. Lam, L. Thiel and S. Swiercz (1989), ‘The nonexistence of finite projective planes of order 10’, Canad. J. Math. 41, 1117–1123. find
  110. N. J. Lehmann (1963), ‘Optimale Eigenwerteinschließung’, Numer. Math. 5, 246– 272. find
  111. X. S. Li, J. W. Demmel, D. H. Bailey, G. Henry, Y. Hida, J. Iskandar, W. Kahan, S. Y. Kang, A. Kapur, M. C. Martin, B. J. Thompson, T. Tung and D. J. Yoo (2002), ‘Design, implementation and testing of extended and mixed precision BLAS’, ACM Trans. Math. Software 28, 152–205. find
  112. E. Loh and W. Walster (2002), ‘Rump’s example revisited’, Reliable Computing 8, 245–248. find
  113. R. Lohner (1988), Einschließung der Lösung gewöhnlicher Anfangs- und Randwert-aufgaben und Anordnungen. PhD thesis, University of Karlsruhe. find
  114. Maple (2009), Release 13, Reference Manual. find
  115. S. Markov and K. Okumura (1999), The contribution of T. Sunaga to interval analysis and reliable computing. In Developments in Reliable Computing (T. Csendes, ed.), Kluwer, pp. 167–188. find
  116. Mathematica (2009), Release 7.0, Reference Manual. find
  117. MATLAB (2004), User’s Guide, Version 7, The MathWorks. find
  118. R. E. Moore (1962), Interval arithmetic and automatic error analysis in digital computing. Dissertation, Stanford University. find
  119. R. E. Moore (1966), Interval Analysis, Prentice-Hall, Englewood Cliffs. find
  120. R. E. Moore (1977), ‘A test for existence of solutions for non-linear systems’, SIAM J. Numer. Anal. 4, 611–615. find
  121. R. E. Moore (1999), ‘The dawning’, Reliable Computing 5, 423–424. find
  122. S. M. Rump Verification methods R. E. Moore, R. B. Kearfott and M. J. Cloud (2009), Introduction To Interval Analysis, Cambridge University Press. find
  123. J.-M. Muller, N. Brisebarre, F. de Dinechin, C.-P. Jeannerod, V. Lefèvre, G. Melquiond, R. Revol, D. Stehlé and S. Torres (2009), Handbook of Floating-Point Arithmetic, Birkhäuser, Boston. find
  124. K. Nagatou, M. T. Nakao and N. Yamamoto (1999), ‘An approach to the numerical verification of solutions for nonlinear elliptic problems with local uniqueness’, Numer. Funct. Anal. Optim. 20, 543–565. find
  125. M. T. Nakao (1988), ‘A numerical approach to the proof of existence of solutions for elliptic problems’, Japan J. Appl. Math. 5, 313–332. find
  126. M. T. Nakao (1993), Solving nonlinear elliptic problems with result verification using an H −1 type residual iteration. Computing (Suppl.) 9, 161–173. find
  127. M. T. Nakao and N. Yamamoto (1995), ‘Numerical verifications for solutions to elliptic equations using residual iterations with higher order finite elements’, J. Comput. Appl. Math. 60, 271–279. find
  128. M. T. Nakao, K. Hashimoto and Y. Watanabe (2005), ‘A numerical method to verify the invertibility of linear elliptic operators with applications to nonlinear problems’, Computing 75, 1–14. find
  129. N. S. Nedialkov (1999), Computing rigorous bounds on the solution of an initial value problem for an ordinary differential equation. PhD dissertation, University of Toronto, Canada. find
  130. N. S. Nedialkov and K. R. Jackson (2000), ODE software that computes guaranteed bounds on the solution. In Advances in Software Tools for Scientic Computing (H. P. Langtangen, A. M. Bruaset and E. Quak, eds), Springer, pp. 197–224. find
  131. NETLIB (2009), Linear Programming Library. http://www.netlib.org/lp. ↗
  132. A. Neumaier (1974), ‘Rundungsfehleranalyse einiger Verfahren zur Summation endlicher Summen’, Z. Angew. Math. Mech. 54, 39–51. find
  133. A. Neumaier (1984), ‘New techniques for the analysis of linear interval equations’, Linear Algebra Appl. 58, 273–325. find
  134. A. Neumaier (1987), ‘Overestimation in linear interval equations’, SIAM J. Numer. Anal. 24, 207–214. find
  135. A. Neumaier (1988), ‘An existence test for root clusters and multiple roots’, Z. Angew. Math. Mech. 68, 256–257. find
  136. A. Neumaier (1989), ‘Rigorous sensitivity analysis for parameter-dependent systems of equations’, J. Math. Anal. Appl. 144, 16–25. find
  137. A. Neumaier (1990), Interval Methods for Systems of Equations, Encyclopedia of Mathematics and its Applications, Cambridge University Press. find
  138. A. Neumaier (1993), ‘The wrapping effect, ellipsoid arithmetic, stability and confidence regions’, Computing Supplementum 9, 175–190. find
  139. A. Neumaier (2001), Introduction to Numerical Analysis, Cambridge University Press. find
  140. A. Neumaier (2002), ‘Grand challenges and scientific standards in interval analysis’, Reliable Computing 8, 313–320. find
  141. A. Neumaier (2003), ‘Enclosing clusters of zeros of polynomials’, J. Comput. Appl. Math. 156, 389–401. find
  142. A. Neumaier (2004), Complete search in continuous global optimization and constraint satisfaction. In Acta Numerica, Vol. 13, Cambridge University Press, pp. 271–369. find
  143. A. Neumaier (2009), FMathL: Formal mathematical language. http://www.mat.univie.ac.at/˜neum/FMathL.html. ↗
  144. A. Neumaier (2010), ‘Improving interval enclosures’, to appear in Reliable Computing. find
  145. A. Neumaier and T. Rage (1993), ‘Rigorous chaos verification in discrete dynamical systems’, Physica D 67, 327–346. find
  146. A. Neumaier and O. Shcherbina (2004), ‘Safe bounds in linear and mixed-integer programming’, Math. Program. A 99, 283–296. find
  147. W. Oettli and W. Prager (1964.), ‘Compatibility of approximate solution of linear equations with given error bounds for coefficients and right-hand sides’, Numer. Math. 6, 405–409 find
  148. T. Ogita, S. Oishi and Y. Ushiro (2001), ‘Fast verification of solutions for sparse monotone matrix equations’, Comput. Suppl. 15, 175–187. find
  149. S. Oishi (1998), private communication. find
  150. S. Oishi (2000), Numerical Methods with Guaranteed Accuracy (in Japanese), Corona-sya. find
  151. S. Oishi and S. M. Rump (2002), ‘Fast verification of solutions of matrix equations’, Numer. Math. 90, 755–773. find
  152. T. Okayama, T. Matsuo and M. Sugihara (2009), Error estimates with explicit constants for sinc approximation, sinc quadrature and sinc indefinite integration. Technical Report METR2009-01, The University of Tokyo. find
  153. J. B. Oliveira and L. H. de Figueiredo (2002) ‘Interval computation of Viswanath’s constant’, Reliable Computing 8, 131–138. find
  154. F. Ordóñez and R. M. Freund (2003), ‘Computational experience and the explanatory value of condition measures for linear optimization’, SIAM J. Optim. 14, 307–333. find
  155. M. Overton (2001), Numerical Computing with IEEE Floating Point Arithmetic, SIAM, Philadelphia. find
  156. A. Ovseevich and F. Chernousko (1987), ‘On optimal ellipsoids approximating reachable sets’, Problems of Control and Information Theory 16, 125–134. find
  157. M. Payne and R. Hanek (1983), ‘Radian reduction for trigonometric functions’, SIGNUM Newsletter 18, 19–24. find
  158. K. Petras (2002), ‘Self-validating integration and approximation of piecewise analytic functions’, J. Comput. Appl. Math. 145, 345–359. find
  159. M. Plum (1992), ‘Numerical existence proofs and explicit bounds for solutions of nonlinear elliptic boundary value problems’, Computing 49, 25–44. find
  160. M. Plum (1994), ‘Enclosures for solutions of parameter-dependent nonlinear elliptic boundary value problems: Theory and implementation on a parallel computer’, Interval Comput. 3, 106–121. find
  161. M. Plum (1995), ‘Existence and enclosure results for continua of solutions of parameter-dependent nonlinear boundary value problems’, J. Comput. Appl. Math. 60, 187–200. find
  162. M. Plum (1996), Enclosures for two-point boundary value problems near bifurcation points. In Scientific Computing and Validated Numerics: Proc. International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, SCAN-95 (G. Alefeld et al., eds), Vol. 90 of Math. Res., Akadem… find
  163. S. M. Rump Verification methods M. Plum (1997), ‘Guaranteed numerical bounds for eigenvalues’, In Spectral Theory and Computational Methods of Sturm–Liouville Problems: Proc. 1996 Conference, Knoxville, TN, USA (D. Hinton et al., eds), Vol. 191 of Lect. Notes Pure Appl. Math., Marcel Dekker, New Yor… find
  164. M. Plum (2008), ‘Existence and multiplicity proofs for semilinear elliptic boundary value problems by computer assistance’, DMV Jahresbericht 110, 19–54. find
  165. M. Plum and C. Wieners (2002), ‘New solutions of the Gelfand problem’, J. Math. Anal. Appl. 269, 588–606. find
  166. S. Poljak and J. Rohn (1993), ‘Checking robust nonsingularity is NP-hard’, Math. Control, Signals, and Systems 6, 1–9. find
  167. L. B. Rall (1981), Automatic Differentiation: Techniques and Applications, Vol. 120 of Lecture Notes in Computer Science, Springer. find
  168. H. Ratschek and J. Rokne (1984), Computer Methods for the Range of Functions, Halsted Press, New York. find
  169. A. Rauh, E. Auer and E. P. Hofer (2006), ValEncIA-IVP: A comparison with other initial value problem solvers. In Proc. 12th GAMM–IMACS International Symposium on Scientific Computing, Computer Arithmetic, and Validated Numerics, SCAN, Duisburg. find
  170. K. Rektorys (1980), Variational methods in mathematics. In Science and Engineering, 2nd edn, Reidel, Dordrecht. find
  171. F. N. Ris (1972), Interval analysis and applications to linear algebra. PhD dissertation, Oxford University. find
  172. R. H. Risch (1969), ‘The problem of integration in finite terms’, Trans. Amer. Math. Soc. 139, 167–189. find
  173. J. Rohn (1994), NP-hardness results for linear algebraic problems with interval data. In Topics in Validated Computations (J. Herzberger, ed.), Studies in Computational Mathematics, Elsevier, Amsterdam, pp. 463–471. find
  174. J. Rohn (2005), A handbook of results on interval linear problems. http://www.cs.cas.cz/rohn/handbook. ↗
  175. J. Rohn (2009a), ‘Forty necessary and sufficient conditions for regularity of interval matrices: A survey’, Electron. J. Linear Algebra 18, 500–512. find
  176. J. Rohn (2009b), VERSOFT: Verification software in MATLAB/INTLAB. http://uivtx.cs.cas.cz/˜rohn/matlab. ↗
  177. J. Rohn and V. Kreinovich (1995), ‘Computing exact componentwise bounds on solutions of linear system is NP-hard’, SIAM J. Matrix Anal. Appl. 16, 415– 420. find
  178. S. M. Rump (1980), Kleine Fehlerschranken bei Matrixproblemen. PhD thesis, Universität Karlsruhe. find
  179. S. M. Rump (1983), Solving algebraic problems with high accuracy. Habilitationsschrift, published in A New Approach to Scientific Computation (U. W. Kulisch and W. L. Miranker, eds), Academic Press, pp. 51–120. find
  180. S. M. Rump (1990), ‘Rigorous sensitivity analysis for systems of linear and non-linear equations’, Math. Comput. 54, 721–736. find
  181. S. M. Rump (1994), Verification methods for dense and sparse systems of equations. In Topics in Validated Computations (J. Herzberger, ed.), Elsevier, Studies in Computational Mathematics, Amsterdam, pp. 63–136. find
  182. S. M. Rump (1999a), INTLAB: INTerval LABoratory. In Developments in Reliable Computing (T. Csendes, ed.), Kluwer, Dordrecht, pp. 77–104. http://www.ti3.tu-harburg.de/rump/intlab/index.html. ↗
  183. S. M. Rump (1999b), ‘Fast and parallel interval arithmetic’, BIT Numer. Math. 39, 539–560. find
  184. S. M. Rump (2001a), Rigorous and portable standard functions. BIT Numer. Math. 41, 540–562. find
  185. S. M. Rump (2001b), ‘Computational error bounds for multiple or nearly multiple eigenvalues’, Linear Algebra Appl. 324, 209–226. find
  186. S. M. Rump (2003a), ‘Ten methods to bound multiple roots of polynomials’, J. Comput. Appl. Math. 156, 403–432. find
  187. S. M. Rump (2003b), ‘Structured perturbations I: Normwise distances’, SIAM J. Matrix Anal. Appl. 25, 1–30. find
  188. S. M. Rump (2003c), ‘Structured perturbations II: Componentwise distances’, SIAM J. Matrix Anal. Appl. 25, 31–56. find
  189. S. M. Rump (2006), ‘Eigenvalues, pseudospectrum and structured perturbations’, Linear Algebra Appl. 413, 567–593. find
  190. S. M. Rump (2009), ‘Ultimately fast accurate summation’, SIAM J. Sci. Comput. 31, 3466–3502. find
  191. S. M. Rump and S. Graillat (2009), Verified error bounds for multiple roots of systems of nonlinear equations. To appear in Numer. Algorithms; published online at Numer Algor DOI 10.1007/s11075-009-9339-3. — [doi:10.1007/s11075-009-9339-3](https://doi.org/10.1007/s11075-009-9339-3) find
  192. S. M. Rump and S. Oishi (2009), Verified error bounds for multiple roots of non-linear equations. In Proc. International Symposium on Nonlinear Theory and its Applications: NOLTA’09. find
  193. S. M. Rump and H. Sekigawa (2009), ‘The ratio between the Toeplitz and the unstructured condition number’, Operator Theory: Advances and Applications 199, 397–419. find
  194. S. M. Rump and J. Zemke (2004), ‘On eigenvector bounds’, BIT Numer. Math. 43, 823–837. find
  195. S. M. Rump, T. Ogita and S. Oishi (2008), ‘Accurate floating-point summation I: Faithful rounding’, SIAM J. Sci. Comput. 31, 189–224. find
  196. N. V. Sahinidis and M. Tawaralani (2005), ‘A polyhedral branch-and-cut approach to global optimization’, Math. Program. B 103, 225–249. find
  197. H. Schichl and A. Neumaier (2004), ‘Exclusion regions for systems of equations’, SIAM J. Numer. Anal. 42, 383–408. find
  198. H. Schichl and A. Neumaier (2005), ‘Interval analysis on directed acyclic graphs for global optimization’, J. Global Optim. 33, 541–562. find
  199. S. P. Shary (2002), ‘A new technique in systems analysis under interval uncertainty and ambiguity’, Reliable Computing 8, 321–419. find
  200. G. W. Stewart (1990), ‘Stochastic perturbation theory’, SIAM Rev. 32, 579–610. find
  201. T. Sunaga (1956), Geometry of numerals. Master’s thesis, University of Tokyo. find
  202. T. Sunaga (1958), ‘Theory of an interval algebra and its application to numerical analysis’, RAAG Memoirs 2, 29–46. find
  203. A. Takayasu, S. Oishi and T. Kubo (2009a), Guaranteed error estimate for solutions to two-point boundary value problem. In Proc. International Symposium on Nonlinear Theory and its Applications: NOLTA’09, pp. 214–217. find
  204. S. M. Rump Verification methods A. Takayasu, S. Oishi and T. Kubo (2009b), Guaranteed error estimate for solutions to linear two-point boundary value problems with FEM. In Proc. find
  205. Asia Simulation Conference 2009 (JSST 2009 ), Shiga, Japan, pp. 1–8. find
  206. M. Tawaralani and N. V. Sahinidis (2004), ‘Global optimization of mixed-integer nonlinear programs: A theoretical and computational study’, Math. Program. 99, 563–591. find
  207. M. J. Todd (2001), Semidefinite programming. In Acta Numerica, Vol. 10, Cambridge University Press, pp. 515–560. find
  208. L. N. Trefethen (2002), ‘The SIAM 100-dollar, 100-digit challenge’, SIAM-NEWS 35, 2. http://www.siam.org/siamnews/06-02/challengedigits.pdf. ↗
  209. L. N. Trefethen and R. Schreiber (1990), ‘Average-case stability of Gaussian elimination’, SIAM J. Matrix Anal. Appl. 11, 335–360. find
  210. W. Tucker (1999), ‘The Lorenz attractor exists’, CR Acad. Sci., Paris, Sér. I, Math. 328, 1197–1202. find
  211. R. H. Tütüncü, K. C. Toh and M. J. Todd (2003), ‘Solving semidefinite-quadratic-linear programs using SDPT3’, Math. Program. B 95, 189–217. find
  212. L. Vandenberghe and S. Boyd (1996), ‘Semidefinite programming’, SIAM Review 38, 49–95. find
  213. J. Vignes (1978), ‘New methods for evaluating the validity of the results of mathematical computations’, Math. Comp. Simul. XX, 227–249. find
  214. J. Vignes (1980), Algorithmes Numériques: Analyse et Mise en Oeuvre 2: Equations et Systèmes Non Linéaires, Collection Langages et Algorithmes de l’Informatique, Editions Technip, Paris. find
  215. D. Viswanath (1999) ‘Random Fibonacci sequences and the number 1.13198824 . . .’, Math. Comp. 69, 1131–1155. find
  216. D. Viswanath and L. N. Trefethen (1998), ‘Condition numbers of random triangular matrices’, SIAM J. Matrix Anal. Appl. 19, 564–581. find
  217. M. Warmus (1956), ‘Calculus of approximations’, Bulletin de l’Academie Polonaise des Sciences 4, 253–259. find
  218. B. Werner and A. Spence (1984), ‘The computation of symmetry-breaking bifurcation points’, SIAM J. Numer. Anal. 21, 388–399. find
  219. J. H. Wilkinson (1965), The Algebraic Eigenvalue Problem, Clarendon Press, Oxford. find
  220. S. J. Wright (1993), ‘A collection of problems for which Gaussian elimination with partial pivoting is unstable’, SIAM J. Sci. Comput. 14, 231–238. find
  221. N. Yamanaka, T. Okayama, S. Oishi and T. Ogita (2009), ‘A fast verified automatic integration algorithm using double exponential formula’, RIMS Kokyuroku 1638, 146–158. find
  222. R. C. Young (1931), ‘The algebra of many-valued quantities’, Mathematische Annalen 104, 260–290. find
  223. Y.-K. Zhu, J.-H. Yong and G.-Q. Zheng (2005), ‘A new distillation algorithm for floating-point summation’, SIAM J. Sci. Comput. 26, 2066–2078. find
  224. G. Zielke and V. Drygalla (2003), ‘Genaue Lösung linearer Gleichungssysteme’, GAMM Mitt. Ges. Angew. Math. Mech. 26, 7–108. find
  225. S. Zimmermann and U. Mertins (1995), ‘Variational bounds to eigenvalues of self-adjoint eigenvalue problems with arbitrary spectrum’, Z. Anal. Anwendungen 14, 327–345. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/rump-2010-verification-methods-rigorous-results-floating/