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

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)