Verification methods: Rigorous results using floating-point arithmetic

DOI10.1017/S096249291000005XzbMath1323.65046MaRDI QIDQ2890535

Publication date: 11 June 2012

Published in: Acta Numerica (Search for Journal in Brave)

Learning and adaptive systems in artificial intelligence (68T05) Mechanization of proofs and logical operations (03B35) Algorithms with automatic result verification (65G20)

Related Items

On an approach to numerical solutions of the Dirichlet problem of an arbitrary dimension, Verified Error Bounds for All Eigenvalues and Eigenvectors of a Matrix, Existence of traveling wave solutions for the Diffusion Poisson Coupled Model: a computer-assisted proof, Numerical verification for solutions to partial differential equations, Fast enclosing the solution set of the parametric Sylvester matrix equations, Validation of the bifurcation diagram in the 2D Ohta–Kawasaki problem, Floating-point arithmetic, Arnold Diffusion, Quantitative Estimates, and Stochastic Behavior in the <scp>Three‐Body</scp> Problem, Computer-Assisted Proof of Shil'nikov Homoclinics: With Application to the Lorenz-84 Model, Enabling floating-point arithmetic in the Coq proof assistant, Validated Root Enclosures for Interval Polynomials with Multiplicities, Verified eigenvalue and eigenvector computations using complex moments and the Rayleigh-Ritz procedure for generalized Hermitian eigenvalue problems, Computer-assisted proof of shear-induced chaos in stochastically perturbed Hopf systems, Fast verified computation for real powers of large matrices with Kronecker structure, Persistence of Periodic Orbits under State-dependent Delayed Perturbations: Computer-assisted Proofs, On the polygonal Faber-Krahn inequality, Numerical analysis of the kinetic equation describing isotropic 4-wave interactions in non-linear physical systems, Fast computation of error bounds for all eigenpairs of a Hermitian and all singular pairs of a rectangular matrix with emphasis on eigen- and singular value clusters, Cyclic symmetry induced pitchfork bifurcations in the diblock copolymer model, Computer assisted proofs for transverse collision and near collision orbits in the restricted three body problem, Computing Semigroups with Error Control, A Posteriori Validation of Generalized Polynomial Chaos Expansions, A review note on arbitrary precision arithmetic, Analytic Continuation of Local (Un)Stable Manifolds with Rigorous Computer Assisted Error Bounds, On bifurcation and local rigidity of triply periodic minimal surfaces in $\protect \mathbb{R}^3$, Rigorously Computing Symmetric Stationary States of the Ohta--Kawasaki Problem in Three Dimensions, The Round Taylor Method, The united stable solution set of interval continuous-time algebraic Riccati equation and veri ed numerical computation of its outer estimation, Primitive Floats in Coq, Computing Enclosures for the Matrix Exponential, Existence of the first magic angle for the chiral model of bilayer graphene, Effective topological degree computation based on interval arithmetic, Mathematically rigorous global optimization in floating-point arithmetic, Unnamed Item, Enclosing Chebyshev Expansions in Linear Time, On the dimension spectrum of infinite subsystems of continued fractions, Determinants of Interval Matrices, Simulating Low Precision Floating-Point Arithmetic, A Four-Leaf Chaotic Attractor of a Three-Dimensional Dynamical System, Free (rational) derivation, On decomposing mixed-mode oscillations and their return maps, Polynomial homotopy continuation on GPUs, An efficient numerical verification method for the Kolmogorov problem of incompressible viscous fluid, Solving equations and optimization problems with uncertainty, Computing enclosures for the matrix Mittag-Leffler function, A general method for computer-assisted proofs of periodic solutions in delay differential problems, Parameterization of unstable manifolds for DDEs: formal series solutions and validated error bounds, Fourier-Taylor parameterization of unstable manifolds for parabolic partial differential equations: formalism, implementation and rigorous validation, Rotation invariant patterns for a nonlinear Laplace-Beltrami equation: a Taylor-Chebyshev series approach, Parametric AE-solution sets to the parametric linear systems with multiple right-hand sides and parametric matrix equation $A(p)X=B(p)$, Enclosing the solution set of parametric interval matrix equation $A(p)X = B(p)$, Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?, Rigorous enclosures of solutions of Neumann boundary value problems, Validated numerics for equilibria of analytic vector fields: Invariant manifolds and connecting orbits, Computer-assisted bifurcation diagram validation and applications in materials science, Methods for verified stabilizing solutions to continuous-time algebraic Riccati equations, Local adaption for approximation and minimization of univariate functions, Fast enclosure for the minimal nonnegative solution to the nonsymmetric T-Riccati equation, Enclosures for the solution set of parametric interval linear systems, Verified inclusions for a nearest matrix of specified rank deficiency via a generalization of Wedin's $\sin (\theta)$ theorem, Beyond the Melnikov method. II: Multidimensional setting, Stability and uniqueness of slowly oscillating periodic solutions to Wright's equation, Fast verified computation for the matrix principal $p$th root, An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems, Combinatorial-topological framework for the analysis of global dynamics, Rigorous computation of non-uniform patterns for the 2-dimensional Gray-Scott reaction-diffusion equation, An efficient approach to solve very large dense linear systems with verified computing on clusters, The Laurent-Horner method for validated evaluation of Chebyshev expansions, On the algebraic solution of fuzzy linear systems based on interval theory, Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case, Relations between various methods for solving linear interval and parametric equations, A new method for computing a $p$-solution to parametric interval linear systems with affine-linear and nonlinear dependencies, The dimension spectrum of conformal graph directed Markov systems, Asymptotically self-similar blowup of the Hou-Luo model for the 3D Euler equations, Efficient approaches for enclosing the united solution set of the interval generalized Sylvester matrix equations, Chaotic motions in the restricted four body problem via Devaney's saddle-focus homoclinic tangle theorem, A functional analytic approach to validated numerics for eigenvalues of delay equations, Fourier-Taylor approximation of unstable manifolds for compact maps: numerical implementation and computer-assisted error bounds, Multiple/arbitrary precision interval computations in C-XSC, Solvers for the verified solution of parametric linear systems, Periodic orbits in Hořava-Lifshitz cosmologies, An efficient algorithm for finding all solutions of nonlinear equations using parallelogram LP test, Fast algorithms for floating-point interval matrix multiplication, Verified bounds for singular values, in particular for the spectral norm of a matrix and its inverse, Validated Computation of Heteroclinic Sets, Computer assisted error bounds for linear approximation of (un)stable manifolds and rigorous validation of higher dimensional transverse connecting orbits, Rigorous numerics for ill-posed PDEs: periodic orbits in the Boussinesq equation, High-precision computation: mathematical physics and dynamics, Floer homology, group orderability, and taut foliations of hyperbolic 3-manifolds, Fast interval matrix multiplication, Verified error bounds for real eigenvalues of real symmetric and persymmetric matrices, Formally verified approximations of definite integrals, A heuristic verification of the degree of the approximate GCD of two univariate polynomials, AE solutions and AE solvability to general interval linear systems, Computer-assisted proofs for radially symmetric solutions of PDEs, Polynomial approximation of one parameter families of (un)stable manifolds with rigorous computer assisted error bounds, Characterizing and approximating eigenvalue sets of symmetric interval matrices, Verified solutions of delay eigenvalue problems, Mixed Precision Block Fused Multiply-Add: Error Analysis and Application to GPU Tensor Cores, Existence proof of unimodal solutions of the Proudman-Johnson equation via interval analysis, Unification and extension of intersection algorithms in numerical algebraic geometry, Accurate quotient-difference algorithm: error analysis, improvements and applications, A numerical verification method for nonlinear functional equations based on infinite-dimensional Newton-like iteration, Computer-assisted equilibrium validation for the diblock copolymer model, Computing the spectral decomposition of interval matrices and a study on interval matrix powers, Estimation of two error components in the numerical solution to the problem of nonisothermal flow of polymer fluid between two coaxial cylinders, Verified error bounds for eigenvalues of geometric multiplicity $q$ and corresponding invariant subspaces, The verification of multiplicity support of a defective eigenvalue of a real matrix, Fast verified computation for the minimal nonnegative solution of the nonsymmetric algebraic Riccati equation, Some unexpected results on the Brillouin singular equation: fold bifurcation of periodic solutions, Computer assisted proof of transverse saddle-to-saddle connecting orbits for first order vector fields, Interval arithmetic over finitely many endpoints, Complexity issues for the symmetric interval eigenvalue problem, A computer-assisted proof of existence of a periodic solution, Formal proofs of rounding error bounds. With application to an automatic positive definiteness check, Spontaneous periodic orbits in the Navier-Stokes flow, Equilibrium validation in models for pattern formation based on Sobolev embeddings, Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach, An interval extension of SMS method for computing weighted Moore-Penrose inverse, Certified numerical algorithm for isolating the singularities of the plane projection of generic smooth space curves, Centered solutions for uncertain linear equations, Real Root Isolation of Polynomial Equations Based on Hybrid Computation, Verified Computations for Hyperbolic 3-Manifolds, The Forthcoming IEEE Standard 1788 for Interval Arithmetic, Verified partial eigenvalue computations using contour integrals for Hermitian generalized eigenproblems, Verified bounds for the determinant of real or complex point or interval matrices, Verified error bounds for singular solutions of nonlinear systems, On approximate solutions of the equations of incompressible magnetohydrodynamics, Validated Saddle-Node Bifurcations and Applications to Lattice Dynamical Systems, An improved verification algorithm for nonlinear systems of equations based on Krawczyk operator, Formally Verified Approximations of Definite Integrals, Computer-assisted proofs in PDE: a survey, Fast verified computation for positive solutions to $\mathcal{M} $-tensor multi-linear systems and Perron vectors of a kind of weakly irreducible nonnegative tensors, Rigorous verification of Hopf bifurcations in functional differential equations of mixed type, Global dynamics in nonconservative nonlinear Schrödinger equations, Inclusion method of optimal constant with quadratic convergence for $H_0^1$-projection error estimates and its applications, Rigorous validation of stochastic transition paths, A study of the apsidal angle and a proof of monotonicity in the logarithmic potential case, \textsf{ORTHOPOLY}: a library for accurate evaluation of series of classical orthogonal polynomials and their derivatives, The monotonicity of the apsidal angle in power-law potential systems, A computer-assisted method for excluding eigenvalues of an elliptic operator linearized at a solution of a nonlinear problem, Oscillatory motions and parabolic manifolds at infinity in the planar circular restricted three body problem

Uses Software