Formally verified roundoff errors using SMT-based certificates and subdivisions

DOI10.1007/978-3-030-30942-8_4MaRDI QIDQ6535941zbMATH OpenFDO

Authors Joachim Bard, Heiko Becker, Eva Darulova

Publication date 14 March 2024

Full work available at URL https://doi.org/10.1007/978-3-030-30942-8_4

zbMATH Keywords

Coqfinite-precisionroundoff errorSMTsubdivision

Mathematics Subject Classification ID

Roundoff error (65G50) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Certified roundoff error bounds using semidefinite programming
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
• Certification of bounds on expressions involving rounded operators
• Formally verified certificate checkers for hardest-to-round computation
• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check

Cites work

• Affine arithmetic: concepts and applications
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Certified roundoff error bounds using semidefinite programming
• scientific article; zbMATH DE number 3281219 (Why is no real title available?)
• Static analysis of finite precision computations

This page was built for publication: Formally verified roundoff errors using SMT-based certificates and subdivisions

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