Verified Real Number Calculations: A Library for Interval Arithmetic

DOI10.1109/TC.2008.213MaRDI QIDQ4975017zbMATH OpenOpenAlexFDO

Authors Marc Daumas, David R. Lester, César 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)

Cited in

(13)

• 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
• MetiTarski: An automatic theorem prover for real-valued special functions
• Affine arithmetic and applications to real-number proving
• Computer-Aided Verification for Iterative Matrix Inversion Problems in Systems and Control
• Proving tight bounds on univariate expressions with elementary functions in Coq
• MetiTarski: An Automatic Prover for the Elementary Functions
• Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
• Formalization of Bernstein polynomials and applications to global optimization
• Formalization of real analysis: a survey of proof assistants and libraries
• Exact real arithmetic for interval number systems
• Coquelicot: a user-friendly library of real analysis for Coq

Describes a project that uses

Uses Software

• PVS

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4975017)