Verification methods: Rigorous results using floating-point arithmetic

Moore, 1966, Interval Analysis

Moore, 1999, The dawning, Reliable Computing, 5, 423, 10.1023/A:1017250200443

10.1137/S1064827594266131

10.4153/CJM-1989-049-4

Anderson, 1995, LAPACK User‘s Guide, Release

10.1137/1.9780898718027

10.1137/S0895479802405744

10.1137/S0895479896312869

10.1007/978-94-017-1247-7_7

Plum, 2008, Existence and multiplicity proofs for semilinear elliptic boundary value problems by computer assistance, DMV Jahresbericht, 110, 19

10.1007/s10107-003-0467-6

10.1137/050622870

Fousse L. , Hanrot G. , Lefèvre V. , Pélissier P. and Zimmermann P. (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.

Alefeld G. , private communication.

Todd, 2001, Acta Numerica, 10, 515

10.1137/S0895479893251198

Jansson, 1994, Topic,s in Validated Computations, 381

Darboux, 1876, Sur les développements en série des fonctions d'une seule variable, J. des Mathématiques Pures et Appl., 3, 291

10.1137/S0895479896313978

NETLIB (2009), Linear Programming Library. http://www.netlib.org/lp.

10.1007/BF03167877

Bünger F. (2008), private communication.

10.1016/0377-0427(94)00091-E

Bernelli Zazzera F. , Vasile M. , Massari M. and Di Lizia P. (2004), Assessing the accuracy of interval arithmetic estimates in space flight mechanics. Final report, Ariadna id: 04/4105, Contract Number: 18851/05/NL/MV.

Eckmann, 1984, A computer-assisted proof of universality for area-preserving maps, Mem. Amer. Math. Soc., 47, 289

10.1137/0610035

Hansen, 1969, Topics in Interval Analysis, 102

10.1137/0704001

Rump S. M. and Oishi S. (2009), Verified error bounds for multiple roots of nonlinear equations. In Proc. International Symposium on Nonlinear Theory and its Applications: NOLTA'09.

Fazekas B. , Plum M. and Wieners C. (2005), Enclosure for biharmonic equation. In Dagstuhl Online Seminar Proceedings 05391. http://drops.dagstuhl.de/portal/05391/.

Lohner R. (1988), Einschlieβung der Lösung gewöhnlicher Anfangs- und Randwertaufgaben und Anordnungen. PhD thesis, University of Karlsruhe.

Galias, 1998, Computer assisted proof of chaos in the Lorenz equations, Physica, 115, 165

10.1007/978-3-7091-6918-6_14

Frommer, 2001, Perspectives on Enclosure Methods: SCAN 2000

10.1137/S0895479802405732

10.1007/BF02307379

10.1007/BF02238302

Kreinovich, 1993, Optimal solution of interval linear systems is intractable (NP-hard), Interval Comput., 1, 6

Rohn, 1994, Topics in Validated Computations, 463

Yamanaka, 2009, A fast verified automatic integration algorithm using double exponential formula, RIMS Kokyuroku, 1638, 146

10.1137/0721029

10.1007/s002110100310

10.1007/3-540-10861-0

10.1137/1.9780898717969

10.1007/BF01213466

10.1023/A:1014702122205

10.1023/A:1015569431383

Behnke H. (1989), Die Bestimmung von Eigenwertschranken mit Hilfe von Variationsmethoden und Intervallarithmetik. Dissertation, Institut für Mathematik, TU Clausthal.

10.1002/zamm.19740540106

10.1007/BF01386090

10.1016/0362-546X(93)90147-K

10.1007/978-3-642-57172-5_6

Rump, 1994, Topics in Validated Computations, 63

10.1007/978-3-662-07964-5

Kearfott, 2005, Proc. XIII Baikal International School-Seminar: Optimization Methods and their Applications, 4

10.1007/s006070170028

10.1016/0378-4754(78)90016-2

Grisvard, 1985, Elliptic Problems in Nonsmooth Domains

10.1016/0024-3795(84)90217-9

1984, IBM High-Accuracy Arithmetic Subroutine Library

2008, ANSI/IEEE 754–2008: IEEE Standard for Floating-Point Arithmetic

10.1145/103162.103163

Knuth, 1969, The Art of Computer Programming: Seminumerical Algorithms, 2

Behnke, 1994, Topics in Validated Computations, 277

10.1137/0724017

10.1007/s10898-005-0937-x

Demmel, 2008, Acta Numerica, 17, 87

10.1137/S0895479896297069

Maple (2009), Release 13, Reference Manual.

Hargreaves G. (2002), Interval analysis in MATLAB. Master's thesis, University of Manchester. http://www.manchester.ac.uk/mims/eprints.

Takayasu A. , Oishi S. and Kubo T. (2009 a), 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.

Andrade M. V. A. , Comba J. L. D. and Stolfi J. (1994), Affine arithmetic. Extended abstract, presented at INTERVAL'94, St. Petersburg.

10.1137/0714040

10.1017/CBO9780511665585

Browne, 1988, Is a math proof a proof if no one can check it?, The New York Times, 1

10.1023/A:1026437523641

10.1016/0024-3795(92)90046-D

10.1145/567806.567808

10.1109/TEC.1961.5219227

10.1016/S0024-3795(96)00681-7

Ovseevich, 1987, On optimal ellipsoids approximating reachable sets, Problems of Control and Information Theory, 16, 125

Neumaier, 2010, Improving interval enclosures, Reliable Computing

Rump, 1999, Fast and parallel interval arithmetic, BIT Numer. Math., 39, 539

10.1016/j.laa.2005.06.009

10.1016/S0764-4442(99)80439-X

Oishi S. (1998), private communication.

10.1016/S0377-0427(02)00693-3

10.1137/1.9780898718829

10.1137/S0895479892239755

10.1137/050645671

10.1023/B:BITN.0000009941.51707.26

Neumaier A. (2009), FMathL: Formal mathematical language. http://www.mat.univie.ac.at/~neum/FMathL.html.

10.1007/s11155-006-9004-7

Bischof C. H. , Carle A. , Corliss G. and Griewank A. (1991), ADIFOR: Generating derivative codes from Fortran programs. Technical report, Mathematics and Computer Science Division, Argonne National Laboratory.

Ladyzhenskaya, 1968, Linear and Quasilinear Elliptic Equations

10.1007/978-1-4613-0075-5

10.1017/S0334270000001077

Adams, 1975, Sobolev Spaces

10.1137/0611023

Alefeld, 1994, Topics in Validated Computations, 7

10.1090/surv/040.1

1986, ARITHMOS: Benutzerhandbuch

10.1515/9783111682457

Rump S. M. and Graillat S. (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.

Beaumont O. (2000), Solving interval linear systems with oblique boxes. Research report PI 1315, INRIA.

10.1080/10556789908805769

Börsken N. C. (1978), Komplexe Kreis-Standardfunktionen. Diplomarbeit, Freiburger Intervall-Ber. 78/2, Institut für Angewandte Mathematik, Universität Freiburg.

Braune K. D. (1987), Hochgenaue Standardfunktionen für reelle und komplexe Punkte und Intervalle in beliebigen Gleitpunktrastern. Dissertation, Univer-sität Karlsruhe.

10.1090/S0025-5718-1990-1011445-5

10.1016/S0022-247X(02)00038-0

10.1016/j.jde.2005.07.016

10.1016/S0022-0396(03)00186-4

10.1016/S0377-0427(00)00481-7

10.1007/BF01947742

Chatelin F. (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.

Griewank, 2003, Acta Numerica, 12, 321

Neumaier, 1990, Interval Methods for Systems of Equations

10.1137/080738490

10.1137/0908069

10.1007/978-3-7091-6217-0_14

Daumas M. , Melquiond G. and Muñoz C. (2005), Guaranteed proofs using interval arithmetic. In Proc. 17th IEEE Symposium on Computer Arithmetic (ARITH'05).

10.1007/BF01397083

Demmel J. B. (1989), On floating point errors in Cholesky. LAPACK Working Note 14 CS–89–87, Department of Computer Science, University of Tennessee, Knoxville, TN, USA.

Plum, 1997, Spectral Theory and Computational Methods of Sturm-Liouville Problems: Proc. 1996 Conference, Knoxville, TN, USA, 191, 313

10.1007/s10208001004

Demmel J. B. , Hida Y. , Kahan W. , Li X. S. , Mukherjee S. and Riedy E. J. (2004), Error bounds from extra precise iterative refinement. Report no. ucb/csd–04–1344, Computer Science Devision (EECS), University of California, Berkeley.

Dwyer, 1951, Linear Computations

Kulisch, 1981, Computer Arithmetic in Theory and Practice

10.1007/BF02288367

Eijgenraam P. (1981), The solution of initial value problems using interval arithmetic.

Alefeld, 1974, Einführung in die Intervallrechnung

10.1023/B:NUMA.0000049462.70970.b6

10.1007/BF01404681

10.1007/BF01221125

Keil, 2006, Algebraic and Numerical Algorithms and Computer-assisted Proofs

10.1007/978-3-642-61798-0

Gordon, 2000, Proof, Language, and Interaction: Essays in Honour of Robin Milner

10.1090/S1079-6762-95-03001-0

10.1023/B:JOGO.0000006720.68398.8c

10.1137/0613014

Hölzl J. (2009), Proving real-valued inequalities by computation in Isabelle/HOL. Diplomarbeit, Fakultät für Informatik der Technischen Universität München.

10.1137/S1052623402416839

Jansson C. (2006), VSDP: A MATLAB software package for verified semidefinite programming. In NOLTA 2006, pp. 327–330.

Krämer W. (1991), Verified solution of eigenvalue problems with sparse matrices. In Proc. 13th World Congress on Computation and Applied Mathematics, pp. 32–33.

10.1007/BF03186539

Kahan W. M. (1968), A more complete interval arithmetic. Lecture notes for a summer course at the University of Michigan.

Kanzawa, 1999, Imperfect singular solutions of nonlinear equations and a numerical method of proving their existence, IEICE Trans. Fundamentals, E82-A, 1062

Kanzawa, 1999, Calculating bifurcation points with guaranteed accuracy, IEICE Trans. Fundamentals, E82-A, 1055

10.1090/S0002-9947-1969-0237477-8

Kato, 1966, Perturbation Theory for Linear Operators

Kearfott, 1992, INTLIB: A portable Fortran-77 elementary function library, Interval Comput., 3, 96

Klatte, 1993, C-XSC A C++ Class Library for Extended Scientific Computing

10.1007/BF01385896

Knüppel O. (1998), PROFIL/BIAS and extensions, Version 2.0. Technical report, Institut für Informatik III, Technische Universität Hamburg-Harburg.

10.1002/(SICI)1097-007X(199701/02)25:1<37::AID-CTA944>3.0.CO;2-G

Krämer W. (1987), Inverse Standardfunktionen für reelle und komplexe Intervallargumente mit a priori Fehlerabschätzung für beliebige Datenformate. Dissertation, Universität Karlsruhe.

10.1007/BF02234767

10.1007/BF02235463

10.1137/0722037

Kreinovich, 2008, Towards a combination of interval and ellipsoid uncertainty, Vych. Techn., 13, 5

10.1007/BF01409991

10.1002/zamm.200310093

10.1007/978-94-017-1247-7_14

10.1007/s10107-003-0433-3

Mathematica (2009), Release 7.0, Reference Manual.

2004, User‘s Guide, Version 7

Okayama T. , Matsuo T. and Sugihara M. (2009), Error estimates with explicit constants for sinc approximation, sinc quadrature and sinc indefinite integration. Technical Report METR2009–01, The University of Tokyo.

Moore R. E. (1962), Interval arithmetic and automatic error analysis in digital computing. Dissertation, Stanford University.

10.1137/1.9780898717716

Muller, 2009, Handbook of Floating-Point Arithmetic

10.1080/01630569908816910

Nakao, 1993, Solving nonlinear elliptic problems with result verification using an H-1 type residual iteration, Computing, 9, 161

Nakao, 1995, Numerical verifications for solutions to elliptic equations using residual iterations with higher order finite elements, J. Comput. Appl. Math., 60, 271, 10.1016/0377-0427(94)00096-J

10.1007/s00607-004-0111-1

Nedialkov N. S. (1999), Computing rigorous bounds on the solution of an initial value problem for an ordinary differential equation. PhD dissertation, University of Toronto, Canada.

10.1002/zamm.19880680629

10.1016/0022-247X(89)90357-0

10.1017/CBO9780511612916

10.1023/A:1016341317043

10.1016/S0377-0427(03)00380-7

Neumaier, 2004, Acta Numerica, 13, 271

Neumaier, 1993, Rigorous chaos verification in discrete dynamical systems, Physica, 67, 327

Oishi, 2000, Numerical Methods with Guaranteed Accuracy

10.1137/S1052623402401804

10.1137/1.9780898718072

10.1145/1057600.1057602

10.1016/S0377-0427(01)00586-6

10.1007/BF02238648

Plum, 1994, Enclosures for solutions of parameter-dependent nonlinear elliptic boundary value problems: Theory and implementation on a parallel computer, Interval Comput., 3, 106

Plum, 1996, Scientific Computing and Validated Numerics: Proc. International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, SCAN-95, 90, 265

Ratschek, 1984, Computer Methods for the Range of Functions

Rauh, 2006, Proc. 12th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic, and Validated Numerics

10.1137/S0036142999361074

Rektorys, 1980, Science and Engineering

Ris F. N. (1972), Interval analysis and applications to linear algebra. PhD dissertation, Oxford University.

Rohn J. (2005), A handbook of results on interval linear problems. http://www.cs.cas.cz/rohn/handbook.

10.13001/1081-3810.1327

Rohn J. (2009 b), VERSOFT: Verification software in MATLAB/INTLAB. http://uivtx.cs.cas.cz/~rohn/matlab.

Wilkinson, 1965, The Algebraic Eigenvalue Problem

Rump S. M. (1980), Kleine Fehlerschranken bei Matrixproblemen. PhD thesis, Universität Karlsruhe.

10.1016/B978-0-12-428660-3.50010-0

10.1023/A:1021971313412

10.1016/S0377-0427(03)00381-9

Rump, 2009, The ratio between the Toeplitz and the unstructured condition number, Operator Theory: Advances and Applications, 199, 397

Sahinidis, 2005, A polyhedral branch-and-cut approach to global optimization, Math. Program., 103, 225, 10.1007/s10107-005-0581-8

10.1137/S0036142902418898

10.1023/A:1020505620702

10.1137/1032121

10.1137/1038003

Sunaga T. (1956), Geometry of numerals. Master‘s thesis, University of Tokyo.

Takayasu A. , Oishi S. and Kubo T. (2009 b), Guaranteed error estimate for solutions to linear two-point boundary value problems with FEM. In Proc. Asia Simulation Conference 2009 (JSST 2009), Shiga, Japan, pp. 1–8.

Trefethen, 2002, The SIAM 100-dollar, 100-digit challenge, SIAM-NEWS, 35, 2

10.1007/s10107-002-0347-5

Vignes, 1980, Algorithmes Numériques: Analyse et Mise en Oeuvre 2: Equations et Systèmes Non Linéaires

10.1090/S0025-5718-99-01145-X

Warmus, 1956, Calculus of approximations, Bulletin de l‘Academie Polonaise des Sciences, 4, 253

10.1137/0914013

10.1007/BF01457934

10.1137/030602009

Zielke, 2003, Genaue Lösung linearer Gleichungssysteme, GAMM Mitt. Ges. Angew. Math. Mech., 26, 7

10.4171/ZAA/677

10.1016/S0024-3795(00)00279-2

10.1007/BF01180013

10.1016/j.jde.2004.07.017

Sunaga, 1958, Theory of an interval algebra and its application to numerical analysis, RAAG Memoirs, 2, 29