Moore, J. Strother; Lynch, Thomas W.; Kaufmann, Matt (September 1998). "A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program". IEEE Transactions on Computers (Washington, DC, USA: IEEE Computer Society) 47 (9): 913–926. doi:10.1109/12.713311.
