Enabling floating-point arithmetic in the Coq proof assistant

DOI10.1007/S10817-023-09679-XMaRDI QIDQ6053846zbMATH OpenFDO

Authors Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux

Publication date 24 October 2023

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/S10817-023-09679-X

zbMATH Keywords

floating-point arithmeticformal proofproof by computation

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A compiled implementation of strong reduction
• A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
• A rigorous ODE solver and Smale's 14th problem
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
• Handbook of floating-point arithmetic
• scientific article; zbMATH DE number 846277 (Why is no real title available?)
• On relative errors of floating-point operations: optimal bounds and applications
• Primitive Floats in Coq
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Refinements for free!
• Verification methods: rigorous results using floating-point arithmetic
• Verification of positive definiteness
• Verified compilation of floating-point computations

Cited in

(3)

• A modeling concept for formal verification of OS-based compositional software
• End-to-end formal verification of a fast and accurate floating-point approximation
• Switched systems in Coq for modeling periodic controllers

This page was built for publication: Enabling floating-point arithmetic in the Coq proof assistant

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