{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:19:41Z","timestamp":1778498381261,"version":"3.51.4"},"reference-count":24,"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:1008665528003","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"7-44","source":"Crossref","is-referenced-by-count":16,"title":["Verifying the SRT Division Algorithm Using Theorem Proving Techniques"],"prefix":"10.1007","volume":"14","author":[{"given":"Edmund M.","family":"Clarke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven M.","family":"German","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xudong","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"194806_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger (Eds.), Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5"},{"key":"194806_CR2","unstructured":"APT Data Services, \u201cPentium bug fiasco costs Intel dear,\u201d Computer Business Review, Jan. 1995."},{"issue":"10","key":"194806_CR3","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, \u201cHigher-radix division using estimates of the divisor and partial remainders,\u201d IEEE Transactions on Computers, Vol. C-17,No. 10, pp. 925\u2013934, Oct. 1968.","journal-title":"IEEE Transactions on Computers"},{"key":"194806_CR4","series-title":"Technical Report","volume-title":"The UT natural deduction prover","author":"W.W. Bledsoe","year":"1983","unstructured":"W.W. Bledsoe, \u201cThe UT natural deduction prover,\u201d Technical Report ATP-17B, Mathematical Department, University of Texas at Austin, TX, 1983."},{"key":"194806_CR5","series-title":"Technical Report","volume-title":"A prover for general inequalities","author":"W.W. Bledsoe","year":"1979","unstructured":"W.W. Bledsoe, P. Bruell, and R. Shostak, \u201cA prover for general inequalities,\u201d Technical Report ATP-40A, Mathematical Department, University of Texas at Austin, TX, 1979."},{"key":"194806_CR6","unstructured":"R.S. Boyer and J.S. Moore, A Computational Logic Handbook, Academic Press, 1988."},{"key":"194806_CR7","unstructured":"E.M. Clarke and S.M. German, Personal communication to H. Ruess, N. Shankar, and M.K. Srivas, 1995."},{"key":"194806_CR8","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, S.M. German, and X. Zhao, \u201cVerifying the SRT division algorithm using theorem proving techniques,\u201d in R. Alur and T. Henzinger (Eds.), Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_62"},{"key":"194806_CR9","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, M. Khaira, and X. Zhao, \u201cWord level symbolic model checking\u2014Avoiding the pentium FDIV error,\u201d Design Automation Conference, June 1996.","DOI":"10.1145\/240518.240640"},{"key":"194806_CR10","unstructured":"E.M. Clarke and X. Zhao, \u201cAnalytica: A theorem prover for mathematica,\u201d The Journal of Mathematica, Vol. 3,No. 1, 1993."},{"key":"194806_CR11","unstructured":"J.H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper & Row, 1986."},{"key":"194806_CR12","unstructured":"S.M. German, \u201cVerification of arithmetic hardware using a symbolic algebra system,\u201d Lecture Notes, March 1995."},{"key":"194806_CR13","unstructured":"S.M. German and Y. Wang, \u201cVerification of parameterized hardware designs,\u201d in Proceedings of International Conference on Computer Design, 1985."},{"key":"194806_CR14","doi-asserted-by":"crossref","unstructured":"J. Joyce and C. Seger, \u201cThe HOL-Voss system: Model-checking inside a general-purpose theorem prover,\u201d 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":"194806_CR15","doi-asserted-by":"crossref","unstructured":"J. O'Leary, M. Leeser, J. Hickey, and M. Aagaard, \u201cNon-restoring integer square root: A case study in design by principled optimization,\u201d in Proceedings of the Theorem Provers in Circuit Design '94, LNCS 901, Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59047-1_42"},{"key":"194806_CR16","doi-asserted-by":"crossref","unstructured":"V. Pratt, \u201cAnatomy of the Pentium bug,\u201d in Proceedings of TAPSOFT '95: Theory and Practice of Software Development, LNCS 915, Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59293-8_189"},{"key":"194806_CR17","doi-asserted-by":"crossref","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas, \u201cAn integration of model checking with automated proof checking,\u201d in Proceedings of the Seventh Workshop on Computer-Aided Verification, 1995.","DOI":"10.1007\/3-540-60045-0_42"},{"key":"194806_CR18","doi-asserted-by":"crossref","unstructured":"H. Ruess, N. Shankar, and M.K. Srivas, \u201cModular verification of SRT division,\u201d preliminary version in T. Henzinger (Eds.), Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, Springer-Verlag, 1996 [1]}, final version in this journal.","DOI":"10.1007\/3-540-61474-5_63"},{"key":"194806_CR19","unstructured":"E. Sacks, \u201cHierarchical inequality reasoning,\u201d Technical Report, MIT Laboratory for Computer Science, 1987."},{"key":"194806_CR20","unstructured":"H.P. Sharangpani and M.L. Barton, \u201cStatistical analysis of floating point flaw in the Pentium processor (1994),\u201d Technical Report, Intel Corporation, Nov. 1994."},{"key":"194806_CR21","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1145\/322033.322034","volume":"24","author":"R. Shostak","year":"1977","unstructured":"R. Shostak, \u201cOn the sup-inf method for proving Presburger formulas,\u201d Journal of the Association for Computing Machinery, Vol. 24, pp. 529\u2013543, 1977.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"194806_CR22","doi-asserted-by":"crossref","unstructured":"G.S. Taylor, \u201cCompatible hardware for division and square root,\u201d in Proceedings of the 5th IEEE Symposium on Computer Arithmetic, May 1981.","DOI":"10.1109\/ARITH.1981.6159293"},{"key":"194806_CR23","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF01383955","volume":"4","author":"D. Verkest","year":"1994","unstructured":"D. Verkest, L. Claesen, and H. De Man, \u201cA proof of the nonrestoring division algorithm and its implementation on an ALU,\u201d Formal Methods in System Design, Vol. 4, pp. 5\u201331, Jan. 1994.","journal-title":"Formal Methods in System Design"},{"key":"194806_CR24","unstructured":"S. Wolfram, Mathematica: A System for Doing Mathematics by Computer, Wolfram Research Inc., 1988."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008665528003.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008665528003\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008665528003.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:29:58Z","timestamp":1754368198000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008665528003"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["194806"],"URL":"https:\/\/doi.org\/10.1023\/a:1008665528003","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}