{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:04:45Z","timestamp":1754481885496},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614746"},{"type":"electronic","value":"9783540685999"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_62","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:40:32Z","timestamp":1330292432000},"page":"111-122","source":"Crossref","is-referenced-by-count":25,"title":["Verifying the SRT division algorithm using theorem proving techniques"],"prefix":"10.1007","author":[{"given":"E. M.","family":"Clarke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S. M.","family":"German","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"X.","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"10_CR1","unstructured":"APT Data Services. Pentium bug fiasco costs Intel dear. Computer Business Review, January 3, 1995."},{"issue":"10","key":"10_CR2","doi-asserted-by":"crossref","first-page":"925","DOI":"10.1109\/TC.1968.226439","volume":"C-17","author":"D. E. Atkins","year":"1968","unstructured":"D. E. Atkins. Higher-radix division using estimates of the divisor and partial remainders. IEEE Transactions on Computers, C-17(10):925\u2013934, October 1968.","journal-title":"IEEE Transactions on Computers"},{"key":"10_CR3","unstructured":"W. W. Bledsoe. The UT natural deduction prover. Technical Report ATP-17B, Mathematical Dept., University of Texas at Austin, 1983."},{"key":"10_CR4","unstructured":"W. W. Bledsoe, P. Bruell, and R. Shostak. A prover for general inequalities. Technical Report ATP-40A, Mathematical Dept., University of Texas at Austin, 1979."},{"key":"10_CR5","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, 1988."},{"key":"10_CR6","unstructured":"E. M. Clarke and X. Zhao. Analytical A theorem prover for Mathematica. The Journal of Mathematica, 3(1), 1993."},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, M. Khaira and X. Zhao. Word Level Symbolic Model Checking \u2014 Avoiding the Pentium FDIV Error. Design Automation Conference, June, 1996.","DOI":"10.1145\/240518.240640"},{"key":"10_CR8","unstructured":"J. H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, 1986."},{"key":"10_CR9","unstructured":"S. M. German. Towards automatic verification of arithmetic hardware. Lecture notes, March 1995."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"J. Joyce and C. Seger. The HOL-Voss system: model-checking inside a general-purpose theorem prover. In Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, HUG '93, LNCS 780. Springer Verlag, 1993.","DOI":"10.1007\/3-540-57826-9_135"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"J. O'Leary, M. Leeser, J. Hickey, and M. Aagaard. Non-restoring integer square root: a case study in design by principled optimization. In Proceedings of the Theorem Provers in Circuit Design '94, LNCS 901. Springer Verlag, 1995.","DOI":"10.1007\/3-540-59047-1_42"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In Proceedings of the Seventh Workshop on Computer-Aided Verification, 1995.","DOI":"10.1007\/3-540-60045-0_42"},{"key":"10_CR13","unstructured":"E. Sacks. Hierarchical inequality reasoning. Technical report, MIT Laboratory for Computer Science, 1987."},{"key":"10_CR14","unstructured":"H. P. Sharangpani and M. L. Barton. Statistical analysis of floating point flaw in the Pentium processor(1994). Technical report, Intel Corporation, November 1994."},{"key":"10_CR15","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1145\/322033.322034","volume":"24","author":"R. Shostak","year":"1977","unstructured":"R. Shostak. On the sup-inf method for proving Presburger formulas. Journal of the Association for Computing Machinery, 24:529\u2013543, 1977.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"G. S. Taylor. Compatible hardware for division and square root. In Proceedings of the the 5th IEEE Symposium on Computer Arithmetic, May 1981.","DOI":"10.1109\/ARITH.1981.6159293"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01383955","volume":"4","author":"D. Verkest","year":"1994","unstructured":"D. Verkest, L. Claesen, and H. De Man. A proof of the nonrestoring division algorithm and its implementation on an ALU. Formal Methods in System Design, 4:5\u201331, January 1994.","journal-title":"Formal Methods in System Design"},{"key":"10_CR18","unstructured":"S. Wolfram. Mathematica: A System for Doing Mathematics by Computer. Wolfram Research Inc., 1988."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_62.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:06:37Z","timestamp":1605647197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_62","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}