A certificate-based approach to formally verified approximations
From MaRDI portal
Publication:5875414
DOI10.4230/LIPIcs.ITP.2019.8OpenAlexW2936040140MaRDI QIDQ5875414
Florent Bréhard, Damien Pous, Assia Mahboubi
Publication date: 3 February 2023
Full work available at URL: https://laas.hal.science/hal-02088529
Related Items (3)
A certificate-based approach to formally verified approximations ⋮ A symbolic-numeric validation algorithm for linear ODEs with Newton-Picard method ⋮ Verified interactive computation of definite integrals
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Formal and efficient primality proofs by use of computer algebra oracles
- Iterative approximation of fixed points
- A Skeptic's approach to combining HOL and Maple
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
- A rigorous ODE solver and Smale's 14th problem
- Autarkic computations in formal proofs
- A verified ODE solver and the Lorenz attractor
- Formally verified approximations of definite integrals
- Motivations for an arbitrary precision interval arithmetic and the MPFI library
- Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach
- Chebyshev interpolation polynomial-based tools for rigorous computing
- Rigorous uniform approximation of D-finite functions using Chebyshev expansions
- Proving Bounds on Real-Valued Functions with Computations
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
- Chaotic Braided Solutions via Rigorous Numerics: Chaos in the Swift–Hohenberg Equation
- A Numerical Verification Method for Solutions of Boundary Value Problems with Local Uniqueness by Banach's Fixed-Point Theorem
- Arb: Efficient Arbitrary-Precision Midpoint-Radius Interval Arithmetic
- Validated and Numerically Efficient Chebyshev Spectral Methods for Linear Ordinary Differential Equations
- A Quartic System with Twenty-Six Limit Cycles
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- Rigorous Numerics for Nonlinear Differential Equations Using Chebyshev Series
- Theorem Proving in Higher Order Logics
- A certificate-based approach to formally verified approximations
This page was built for publication: A certificate-based approach to formally verified approximations