Formally verified roundoff errors using SMT-based certificates and subdivisions

DOI10.1007/978-3-030-30942-8_4zbMATH Open1539.68148MaRDI QIDQ6535941FDOQ6535941

Authors: Joachim Bard, Heiko Becker, Eva Darulova 

Publication date: 14 March 2024

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

zbMATH Keywords

SMTsubdivisionCoqroundoff errorfinite-precision

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)

Cites Work

• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Title not available (Why is that?)
• Affine arithmetic: concepts and applications
• Static analysis of finite precision computations
• Certified roundoff error bounds using semidefinite programming

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)