Verified Real Number Calculations: A Library for Interval Arithmetic
From MaRDI portal
Publication:4975017
DOI10.1109/TC.2008.213zbMATH Open1367.65213OpenAlexW2132303335MaRDI QIDQ4975017FDOQ4975017
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
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
- Affine arithmetic and applications to real-number proving
- MetiTarski: An automatic theorem prover for real-valued special functions
- 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
Uses Software
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)
