Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
From MaRDI portal
Publication:3613400
DOI10.1007/11814771_6zbMath1222.65156OpenAlexW1535070383MaRDI QIDQ3613400
Publication date: 12 March 2009
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11814771_6
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Floating-point arithmetic on the test bench. How are verified numerical solutions calculated? ⋮ Floating-point arithmetic ⋮ Error bounds on complex floating-point multiplication with an FMA ⋮ Formal verification of numerical programs: from C annotated programs to mechanical proofs ⋮ Some issues related to double rounding ⋮ Combining Coq and Gappa for Certifying Floating-Point Programs
This page was built for publication: Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
