{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T08:29:44Z","timestamp":1765355384740},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40922-x_3","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T04:41:36Z","timestamp":1196311296000},"page":"22-55","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor"],"prefix":"10.1007","author":[{"given":"David M.","family":"Russinoff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"unstructured":"Institute of Electrical and Electronic Engineers, \u201cIEEE Standard for Binary Floating Point Arithmetic\u201d, Std. 754-1985, New York, NY, 1985.","key":"3_CR1"},{"unstructured":"Intel Corporation, Pentium Family User\u2019s Manual, Volume 3: Architecture and Programming Manual, 1994.","key":"3_CR2"},{"doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., and Moore, J, Computer-Aided Reasoning: an Approach, Kluwer Academic Press, 2000.","key":"3_CR3","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"3_CR4","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1109\/12.713311","volume":"47","author":"J Moore","year":"1998","unstructured":"Moore, J, Lynch, T., and Kaufmann, M., \u201cA Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating Point Division Algorithm\u201d, IEEE Transactions on Computers, 47:9, September, 1998.","journal-title":"IEEE Transactions on Computers"},{"unstructured":"Oberman, S., Hesham, A., and Flynn, M., \u201cThe SNAP Project: Design of Floating Point Arithmetic Units\u201d, Computer Systems Lab., Stanford U., 1996.","key":"3_CR5"},{"issue":"1","key":"3_CR6","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008669628911","volume":"14","author":"D. Russinoff","year":"1999","unstructured":"Russinoff, D., \u201cA Mechanically Checked Proof of IEEE Compliance of the AMD-K5 Floating Point Square Root Microcode\u201d, Formal Methods in System Design\n                           14 (1):75\u2013125, January 1999. See \n                    http:\/\/www.onr.com\/user\/russ\/david\/fsqrt.html\n                    \n                  .","journal-title":"Formal Methods in System Design"},{"unstructured":"Russinoff, D., \u201cA Mechanically Checked Proof of IEEE Compliance of the AMD-K7 Floating Point Multiplication, Division, and Square Root Algorithms\u201d. See \n                    http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html\n                    \n                  .","key":"3_CR7"},{"unstructured":"Russinoff, D. and Flatau, A., \u201cRTL Verification: A Floating-Point Multiplier\u201d, in Kaufmann, M., Manolios, P., and Moore, J, eds., Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Press, 2000. See \n                    http:\/\/www.onr.com\/user\/russ\/david\/acl2.html\n                    \n                  .","key":"3_CR8"},{"unstructured":"Russinoff, D., \u201cAn ACL2 Library of Floating-Point Arithmetic\u201d, 1999. See \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/others\/fp-README.html\n                    \n                  .","key":"3_CR9"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T07:44:36Z","timestamp":1580283876000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}