Formally verified roundoff error bounds on LogSumExp-based computations
From MaRDI portal
Cites work
- -complete decision procedures for satisfiability over the reals
- A three-tier strategy for reasoning about floating-point numbers in SMT
- Accuracy and Stability of Numerical Algorithms
- Accurately computing the log-sum-exp and softmax functions
- Automating the verification of floating-point programs
- Bits and Bugs
- Building high integrity applications with SPARK
- C-language floating-point proofs layered with VST and Flocq
- Certification of bounds on expressions involving rounded operators
- Certified roundoff error bounds using semidefinite programming
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Floating-point arithmetic
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Formal proof of a wave equation resolution scheme: the method error
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Handbook of floating-point arithmetic
- Metalibm: a mathematical functions code generator
- MetiTarski: An automatic theorem prover for real-valued special functions
- Modular inference of subprogram contracts for safety checking
- Multi-prover verification of floating-point programs
- On relative errors of floating-point operations: optimal bounds and applications
- Parallel robots.
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Static analysis of finite precision computations
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
This page was built for publication: Formally verified roundoff error bounds on LogSumExp-based computations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7288567)
