Pages that link to "Item:Q4230664"
From MaRDI portal
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<sup>™</sup> Processor (Q4230664):
Displaying 13 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 parametric error analysis of Goldschmidt's division algorithm (Q1765225) (← 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)
