A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode

David M. Russinoff. A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode. Formal Methods in System Design, 14(1):75-125, 1999.

Bibliographies