A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
From MaRDI portal
Publication:4230664
DOI10.1112/S1461157000000176zbMath0910.68008OpenAlexW2099571283MaRDI QIDQ4230664
Publication date: 8 February 1999
Published in: LMS Journal of Computation and Mathematics (Search for Journal in Brave)
Full work available at URL: http://www.lms.ac.uk/jcm/1/
Computing methodologies and applications (68U99) Mathematical problems of computer architecture (68M07) Computer aspects of numerical algorithms (65Y99)
Related Items
Ordinal arithmetic: Algorithms and mechanization, A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures, Efficient and accurate computation of upper bounds of approximation errors, Formal verification of numerical programs: from C annotated programs to mechanical proofs, Deciding floating-point logic with abstract conflict driven clause learning, A parametric error analysis of Goldschmidt's division algorithm, Floating-point arithmetic in the Coq system, Integrating external deduction tools with ACL2, Hardware-Dependent Proofs of Numerical Programs, Formal Verification for High-Assurance Behavioral Synthesis, Verified compilation of floating-point computations, Formal verification of the VAMP floating point unit, Choosing starting values for certain Newton-Raphson iterations
Uses Software
Cites Work
