Last update: Thu Sep 27 02:36:16 MDT 2018
@Article{Russinoff:1998:MCP, author = "David M. Russinoff", title = "A mechanically checked proof of {IEEE} compliance of the floating point multiplication, division and square root algorithms of the {AMD-K7{\TM}} processor", journal = j-LMS-J-COMPUT-MATH, volume = "1", pages = "148--200", year = "1998", CODEN = "????", DOI = "https://doi.org/10.1112/S1461157000000176", ISSN = "1461-1570", ISSN-L = "1461-1570", MRclass = "68M07 (65Y99 68T15)", MRnumber = "99m:68015", MRreviewer = "J. Michel Muller", bibdate = "Fri Nov 29 08:13:48 2002", bibsource = "http://journals.cambridge.org/action/displayJournal?jid=JCM; http://www.math.utah.edu/pub/tex/bib/lms-j-comput-math.bib", note = "Appendices A and B available to subscribers electronically (http://www.lms.ac.uk/jcm/1/lms98001/appendix-a/ and http://www.lms.ac.uk/jcm/1/lms98001/appendix-b/)", URL = "http://www.lms.ac.uk/jcm/1/lms1998-001/", acknowledgement = ack-nhfb, ajournal = "LMS J. Comput. Math.", fjournal = "LMS Journal of Computation and Mathematics", journal-URL = "http://journals.cambridge.org/action/displayJournal?jid=JCM", onlinedate = "01 February 2010", }