{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:17:49Z","timestamp":1755217069782,"version":"3.43.0"},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1999,1]]},"DOI":"10.1023\/a:1008669628911","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"75-125","source":"Crossref","is-referenced-by-count":37,"title":["A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode"],"prefix":"10.1007","volume":"14","author":[{"given":"David M.","family":"Russinoff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"194808_CR1","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J. Moore, A Computational Logic Handbook, Academic Press, Boston, MA, 1988."},{"key":"194808_CR2","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, Verification of arithmetic functions with binary moment diagrams, Technical Report CMU-CS\u201394\u2013160, School of Computer Science, Carnegie-Mellon University, 1994.","DOI":"10.21236\/ADA281028"},{"key":"194808_CR3","unstructured":"E.M. Clarke and X. Zhao, Word level symbolic model checking: A new approach for verifying arithmetic circuits, Technical Report CMU-CS\u201395\u2013161, School of Computer Science, Carnegie-Mellon University, 1995."},{"key":"194808_CR4","doi-asserted-by":"crossref","unstructured":"J. Harrison, Floating point verification in HOL, in Proc. 8th Intl. Workshop on Higher Order Logic Theorem Proving and its Applications, Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60275-5_65"},{"key":"194808_CR5","unstructured":"Institute of Electrical and Electronic Engineers, IEEE standard for binary floating point arithmetic, Std. 754\u20131985, New York, NY, 1985."},{"key":"194808_CR6","unstructured":"Intel Corporation, Pentium Family User's Manual, Vol. 3: Architecture and Programming Manual, 1994."},{"key":"194808_CR7","unstructured":"M. Kaufmann and J. Moore, A precise description of the ACL2 logic, http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/reports\/km97a.ps"},{"key":"194808_CR8","unstructured":"M. Leeser and J. O'Leary, Verification of a subtractive Radix-2 square root algorithm and implementation, in Proc. Intl. Conf. on Computer Design, 1995."},{"key":"194808_CR9","doi-asserted-by":"crossref","unstructured":"P. Miner and J. Leathrum, Verification of IEEE compliant subtractive division algorithms, in M. Srivas and A. Camilleri (Eds.), Proceedings of Formal Methods in Computer-Aided Design (FMCAD) '96, Springer-Verlag LNCS 1166, pp. 275\u2013293, 1996.","DOI":"10.1007\/BFb0031800"},{"key":"194808_CR10","unstructured":"J. Moore, T. Lynch, and M. Kaufmann, A mechanically checked proof of the correctness of the kernel of the AMD5K 86 floating-point division algorithm, http:\/\/devil.ece.utexas.edu\/lynch\/divide\/divide.html"},{"key":"194808_CR11","doi-asserted-by":"crossref","unstructured":"H. Rue\u00df, M.K. Srivas, and N. Shankar, Modular verification of SRT division, in R. Alur and T. Henzinger (Eds.), Computer-Aided Verification (CAV '96), Springer Verlag LNCS 1102, pp. 123\u2013134, July 1996.","DOI":"10.1007\/3-540-61474-5_63"},{"key":"194808_CR12","unstructured":"D.M. Russinoff, A mechanically checked proof of IEEE compliance of the AMD K7 floating point multiplication, division, and square root instructions, http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.ps."},{"key":"194808_CR13","unstructured":"G.L. Steele, Jr., Common Lisp The Language, 2nd edition, Digital Press, 1990."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008669628911.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008669628911\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008669628911.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:51:12Z","timestamp":1754369472000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008669628911"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["194808"],"URL":"https:\/\/doi.org\/10.1023\/a:1008669628911","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}