{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:02:57Z","timestamp":1743127377160,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":13,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781441915382"},{"type":"electronic","value":"9781441915399"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-4419-1539-9_2","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T00:26:11Z","timestamp":1267489571000},"page":"23-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Mechanically Verified Commercial SRT Divider"],"prefix":"10.1007","author":[{"given":"David M.","family":"Russinoff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,1,23]]},"reference":[{"unstructured":"ACL2 Web site. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/","key":"2_CR1_2"},{"key":"2_CR2_2","volume-title":"Verification of arithmetic circuits with binary moment diagrams","author":"RE Bryant","year":"1996","unstructured":"Bryant RE, Chen YA (1996) Verification of arithmetic circuits with binary moment diagrams. In: Proceedings of the 32nd design automation conference, San Francisco, CA, June 1996"},{"issue":"1","key":"2_CR3_2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008665528003","volume":"14","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, German SM, Zhou X (1999) Verifying the SRT division algorithm using theorem proving techniques. Formal Methods Syst Des 14(1):7\u201344. http:\/\/www-2.cs.cmu.edu\/~modelcheck\/ed-papers\/VtSRTDAU.pdf","journal-title":"Formal Methods Syst Des"},{"issue":"3\/4","key":"2_CR4_2","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1147\/rd.483.0311","volume":"48","author":"G Gerwig","year":"2004","unstructured":"Gerwig G, Wetter H, Schwarz EM, Haess J, Krygowski CA, Fleischer BM, Kroener M (2004) The IBM eServer z990 floating-point unit. IBM J Res Dev 48(3\/4):311\u2013322. http:\/\/www.research.ibm.com\/journal\/rd\/483\/gerwig.html","journal-title":"IBM J Res Dev"},{"doi-asserted-by":"crossref","unstructured":"Kapur D, Subramaniam M (1997) Mechanizing verification of arithmetic circuits: SRT division. In: Invited Talk, Proceedings of FSTTCS-17, Kharagpur, India, LNCS 1346. Springer, New York, pp 103\u2013122. http:\/\/www.cs.unm.edu\/~kapur\/myabstracts\/fsttcs97.html","key":"2_CR5_2","DOI":"10.1007\/BFb0058026"},{"key":"2_CR6_2","volume-title":"Computer arithmetic: algorithms and hardware designs","author":"B Parhami","year":"2000","unstructured":"Parhami B (2000) Computer arithmetic: algorithms and hardware designs. Oxford University Press, Oxford"},{"doi-asserted-by":"crossref","unstructured":"Pratt V (1995) Anatomy of the pentium bug. In: TAPSOFT \u201995: theory and practice of software development, LNCS 915. Springer, Heidelberg. https:\/\/eprints.kfupm.edu.sa\/25851\/1\/25851.pdf","key":"2_CR7_2","DOI":"10.1007\/3-540-59293-8_189"},{"key":"2_CR8_2","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1109\/TEC.1958.5222579","volume":"EC-7","author":"JE Robertson","year":"1958","unstructured":"Robertson JE (1958) A new class of digital division methods. IRE Trans Electron Comput EC-7:218\u2013222","journal-title":"IRE Trans Electron Comput"},{"issue":"1","key":"2_CR9_2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1008617612073","volume":"14","author":"H Ruess","year":"1999","unstructured":"Ruess H, Shankar N (1999) Modular verification of SRT division. Formal Methods Syst Des 14(1):45\u201373. http:\/\/www.csl.sri.com\/papers\/srt-long\/srt-long.ps.gz","journal-title":"Formal Methods Syst Des"},{"unstructured":"Russinoff DM (2007) A formal theory of register-transfer logic and computer arithmetic. http:\/\/www.russinoff.com\/libman\/","key":"2_CR10_2"},{"unstructured":"Russinoff DM (2005) Formal verification of floating-point RTL at AMD using the ACL2 theorem prover, IMACS World Congress, Paris, 2005. http:\/\/www.russinoff.com\/papers\/paris.html","key":"2_CR11_2"},{"key":"2_CR12_2","volume-title":"Compatible hardware for division and square root. In: Proceedings of the 5th symposium on computer arithmetic","author":"GS Taylor","year":"1981","unstructured":"Taylor GS (1981) Compatible hardware for division and square root. In: Proceedings of the 5th symposium on computer arithmetic. IEEE Computer Society, Washington, DC"},{"issue":"3","key":"2_CR13_2","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1093\/qjmam\/11.3.364","volume":"11","author":"KD Tocher","year":"1958","unstructured":"Tocher KD (1958) Techniques of multiplication and division for automatic binary computers. Q J Mech Appl Math 11(3):364\u2013384","journal-title":"Q J Mech Appl Math"}],"container-title":["Design and Verification of Microprocessor Systems for High-Assurance Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-1539-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T03:21:36Z","timestamp":1676690496000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-1539-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781441915382","9781441915399"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_2","relation":{},"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"23 January 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}