Pages that link to "Item:Q4230664"

The following pages link to A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor (Q4230664):

Displaying 17 items.

• Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
• Efficient and accurate computation of upper bounds of approximation errors (Q633637) (← links)
• Floating-point arithmetic in the Coq system (Q714617) (← links)
• Formal verification of the VAMP floating point unit (Q816201) (← links)
• Choosing starting values for certain Newton-Raphson iterations (Q817866) (← links)
• Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
• A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures (Q877828) (← links)
• Integrating external deduction tools with ACL2 (Q1006728) (← links)
• A proof of the nonrestoring division algorithm and its implementation on an ALU (Q1314510) (← links)
• A parametric error analysis of Goldschmidt's division algorithm (Q1765225) (← links)
• Formal verification of square root algorithms (Q1870226) (← links)
• Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
• Verified compilation of floating-point computations (Q2352505) (← links)
• Hardware-Dependent Proofs of Numerical Programs (Q3100216) (← links)
• Formal Verification for High-Assurance Behavioral Synthesis (Q3648710) (← links)
• Automated proofs of object code for a widely used microprocessor (Q4371519) (← links)
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program (Q4571480) (← links)