Formal verification of iterative algorithms in microprocessors. - Mark D. Aagaard; Robert B. Jones; Roope Kaivola; Katherine R. Kohatsu; Carl-Johan H. Seger (DAC, 2000)

Proof Engineering in the Large: Formal Verification of Pentium® 4 Floating-Point Divider. - Roope Kaivola; Katherine R. Kohatsu (CHARME, 2001)

Proof engineering in the large: formal verification of Pentium?4 floating-point divider. - Roope Kaivola; Katherine R. Kohatsu (Int. J. Softw. Tools Technol. Transf., 2003)