Verified Real Number Calculations: A Library for Interval Arithmetic

DOI10.1109/TC.2008.213zbMath1367.65213OpenAlexW2132303335MaRDI QIDQ4975017

Marc Daumas, David R. Lester, César A. Muñoz

Publication date: 8 August 2017

Published in: IEEE Transactions on Computers (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/tc.2008.213

Mathematics Subject Classification ID

Numerical algorithms for computer arithmetic, etc. (65Y04)

Related Items (12)

Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Computer-Aided Verification for Iterative Matrix Inversion Problems in Systems and Control ⋮ Proving tight bounds on univariate expressions with elementary functions in Coq ⋮ Affine Arithmetic and Applications to Real-Number Proving ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ MetiTarski: An automatic theorem prover for real-valued special functions ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers ⋮ MetiTarski: An Automatic Prover for the Elementary Functions ⋮ Formalization of Bernstein polynomials and applications to global optimization

Uses Software

• PVS

This page was built for publication: Verified Real Number Calculations: A Library for Interval Arithmetic