Verified Real Number Calculations: A Library for Interval Arithmetic
From MaRDI portal
Publication:4975017
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
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
This page was built for publication: Verified Real Number Calculations: A Library for Interval Arithmetic
