Taming floating-point rounding errors with proofs (invited talk)

DOI10.4230/LIPICS.ITP.2025.41MaRDI QIDQ7323702zbMATH OpenFDO

Authors Laura Titolo

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.41

Mathematics Subject Classification ID

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

Cites work

• A formal analysis of the compact position reporting algorithm
• A formally verified floating-point implementation of the compact position reporting algorithm
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Automatic Generation of Guard-Stable Floating-Point Code
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• Provably correct floating-point implementation of a point-in-polygon algorithm

This page was built for publication: Taming floating-point rounding errors with proofs (invited talk)

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