A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
From MaRDI portal
Publication:4571480
DOI10.1109/12.713311zbMath1392.68051OpenAlexW2108776769WikidataQ55967722 ScholiaQ55967722MaRDI QIDQ4571480
J. Strother Moore, Thomas Lynch, Matt Kaufmann
Publication date: 9 July 2018
Published in: IEEE Transactions on Computers (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1109/12.713311
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (11)
Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic” ⋮ CoSMed: a confidentiality-verified social media platform ⋮ Floating-point arithmetic ⋮ Efficient and accurate computation of upper bounds of approximation errors ⋮ Applications of real number theorem proving in PVS ⋮ Deciding floating-point logic with abstract conflict driven clause learning ⋮ Multi-Prover Verification of Floating-Point Programs ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ Integrating external deduction tools with ACL2 ⋮ Proving the correctness of client/server software ⋮ Additive symmetries: The non-negative case.
This page was built for publication: A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
