{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:50:36Z","timestamp":1759146636874,"version":"3.43.0"},"reference-count":36,"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:1008617612073","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"45-73","source":"Crossref","is-referenced-by-count":7,"title":["Modular Verification of SRT Division"],"prefix":"10.1007","volume":"14","author":[{"given":"Harald","family":"Ruess","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mandayam K.","family":"Srivas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"194807_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification, CAV '96","year":"1996","unstructured":"R. Alur and T.A. Henzinger (Eds.), Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, Springer-Verlag, 1996."},{"issue":"10","key":"194807_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, \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":"194807_CR3","unstructured":"W.W. Bledsoe, \u201cThe SUP-INF method in Presburger arithmetic,\u201d Technical Report Memo ATP-18, The University of Texas at Austin, Math Department, Dec. 1974."},{"key":"194807_CR4","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, \u201cBit-level analysis of an SRT divider circuit,\u201d in Proceedings of the 33rd Design Automation Conference, Las Vegas, NV, pp. 661\u2013665, June 1996.","DOI":"10.1109\/DAC.1996.545657"},{"key":"194807_CR5","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and Y.-A. Chen, \u201cVerification of arithmetic circuits with binary moment diagrams,\u201d in Proceedings of the 32nd Design Automation Conference, San Francisco, CA, pp. 535\u2013541, June 1996.","DOI":"10.1145\/217474.217583"},{"key":"194807_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/BFb0031797","volume-title":"Formal Methods in Computer-Aided Design (FMCAD '96)","author":"Y.-A. Chen","year":"1996","unstructured":"Y.-A. Chen, E. Clarke, P.-H. Ho, Y. Hoskote, T. Kam, M. Khaira, J. O'Leary, and X. Zhao, \u201cVerification of all circuits in a floating-point unit using word-level model checking,\u201d in M. Srivas and A. Camilleri (Eds.), Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of Lecture Notes in Computer Science, Palo Alto, CA, Springer-Verlag, pp. 19\u201333, 1996."},{"issue":"12","key":"194807_CR7","doi-asserted-by":"crossref","first-page":"1529","DOI":"10.1109\/43.180266","volume":"11","author":"S.-K. Chin","year":"1992","unstructured":"S.-K. Chin, \u201cVerified functions for generating signed-binary arithmetic hardware,\u201d IEEE Transactions on Computer-Aided Design, Vol. 11,No. 12, pp. 1529\u20131558, Aug. 1992.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"194807_CR8","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.21236\/ADA296684","volume-title":"Hybrid decision diagrams: Overcoming the limitations of MTBDDs and BMDs","author":"E.M. Clarke","year":"1995","unstructured":"E.M. Clarke, M. Fujita, and X. Zhao, \u201cHybrid decision diagrams: Overcoming the limitations of MTBDDs and BMDs,\u201d Technical Report CMU-CS\u201395\u2013159, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, April 1995."},{"key":"194807_CR9","unstructured":"E.M. Clarke and S.M. German, Personal Communication, 1995."},{"key":"194807_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-61474-5_62","volume-title":"Computer-Aided Verification, CAV '96","author":"E.M. Clarke","year":"1996","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.A. Henzinger (Eds.), Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, Springer-Verlag, pp. 111\u2013122, 1996."},{"key":"194807_CR11","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, M. Khaira, and X. Zhao, \u201cWord level symbolic model checking\u2014Avoiding the Pentium FDIV error,\u201d in Proceedings of the 33rd Design Automation Conference, Las Veqas, NV, pp. 645\u2013648, June 1996.","DOI":"10.1109\/DAC.1996.545654"},{"key":"194807_CR12","series-title":"Lecture Notes in Computer Science","first-page":"203","volume-title":"Theorem Provers in Circuit Design (TPCD '94)","author":"D. Cyrluk","year":"1994","unstructured":"D. Cyrluk, S. Rajan, N. Shankar, and M.K. Srivas, \u201cEffective theorem proving for hardware verification,\u201d in R. Kumar and T. Kropf (Eds.), Theorem Provers in Circuit Design (TPCD '94), volume 910 of Lecture Notes in Computer Science, Bad Herrenalb, Germany, Springer-Verlag, pp. 203\u2013222, Sept. 1994."},{"key":"194807_CR13","unstructured":"S.M. German, Towards Automatic Verification of Arithmetic Hardware, Lecture Notes, March 1995."},{"key":"194807_CR14","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"194807_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/3-540-63166-6_12","volume-title":"Computer-Aided Verification, CAV '97","author":"G. Kamhi","year":"1997","unstructured":"G. Kamhi, O. Weissberg, L. Fix, Z. Binyamini, and Z. Shtadler, \u201cAutomatic datapath extraction for efficient usage of HDDs,\u201d in O. Grumberg (Ed.), Computer-Aided Verification, CAV '97, volume 1254 of Lecture Notes in Computer Science, Haifa, Israel, Springer-Verlag, pp. 95\u2013106, June 1997."},{"key":"194807_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-61474-5_64","volume-title":"Computer-Aided Verification, CAV '96","author":"D. Kapur","year":"1996","unstructured":"D. Kapur and M. Subramaniam, \u201cMechanically verifying a family of multiplier circuits,\u201d in R. Alur and T.A. Henzinger (Eds.), Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, Springer-Verlag, pp. 135\u2013146, 1996."},{"key":"194807_CR17","doi-asserted-by":"crossref","unstructured":"M. Leeser and J. O'Leary, \u201cVerification of a subtractive radix-2 square root algorithm and implementation,\u201d in Proc. of ICCD'95, IEEE Computer Society Press, pp. 526\u2013531, 1995.","DOI":"10.1109\/ICCD.1995.528918"},{"key":"194807_CR18","doi-asserted-by":"crossref","unstructured":"O.L. McSorley, \u201cHigh-speed arithmetic in binary computers,\u201d in Proc. of IRE, pp. 67\u201391, 1961.","DOI":"10.1109\/JRPROC.1961.287779"},{"key":"194807_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/BFb0031800","volume-title":"Formal Methods in Computer-Aided Design (FMCAD '96)","author":"P.S. Miner","year":"1996","unstructured":"P.S. Miner and J.F. Leathrum, Jr., \u201cVerification of IEEE compliant subtractive division algorithms,\u201d in M. Srivas and A. Camilleri (Eds.), Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of Lecture Notes in Computer Science, Palo Alto, CA, Springer-Verlag, pp. 64\u201378, 1996."},{"key":"194807_CR20","unstructured":"J.S. Moore, T. Lynch, and M. Kaufmann, \u201cA mechanically checked proof of the correctness of the kernel of the AMD5K 86 floating-point division algorithm,\u201d IEEE Transactions on Computers, 1997, to appear."},{"key":"194807_CR21","doi-asserted-by":"crossref","unstructured":"S.F. Oberman and M.J. Flynn, \u201cDesign issues in division and other floating-point operations,\u201d IEEE Transactions on Computers, Feb. 1997.","DOI":"10.1109\/12.565590"},{"key":"194807_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/BFb0035400","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS '97)","author":"S. Owre","year":"1997","unstructured":"S. Owre, J. Rushby, and N. Shankar, \u201cIntegration in PVS: Tables, types, and model checking,\u201d in Ed Brinksma (Ed.), Tools and Algorithms for the Construction and Analysis of Systems (TACAS '97), volume 1217 of Lecture Notes in Computer Science, Enschede, The Netherlands, Springer-Verlag, pp. 366\u2013383, April 1997."},{"issue":"2","key":"194807_CR23","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke, \u201cFormal verification for fault-tolerant architectures: prolegomena to the design of PVS,\u201d IEEE Transactions on Software Engineering, Vol. 21,No. 2, pp. 107\u2013125, Feb. 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"194807_CR24","unstructured":"D.L. Parnas, \u201cUsing mathematical models in the inspection of critical software,\u201d in M.G. Hinchey and J.P. Bowen (Eds.), Applications of Formal Methods, International Series in Computer Science, chap. 2, Prentice Hall, pp. 17\u201331, 1995."},{"key":"194807_CR25","doi-asserted-by":"crossref","unstructured":"V. Pratt, \u201cAnatomy of the pentium bug,\u201d in P.D. Mosses, M. Nielsen, and M.I. Schwartzbach (Eds.), TAPSOFT'95: Theory and Practice of Software Development, number 915 in Lecture Notes in Computer Science, Springer-Verlag, pp. 97\u2013107, May 1995.","DOI":"10.1007\/3-540-59293-8_189"},{"key":"194807_CR26","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1109\/TEC.1958.5222579","volume":"EC-7","author":"J.E. Robertson","year":"1958","unstructured":"J.E. Robertson, \u201cA new class of digital division methods,\u201d IRE Trans. on Electron. Computers, Vol. EC-7, pp. 218\u2013222, 1958.","journal-title":"IRE Trans. on Electron. Computers"},{"key":"194807_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BFb0031801","volume-title":"Formal Methods in Computer-Aided Design (FMCAD '96)","author":"H. Rue\u00df","year":"1996","unstructured":"H. Rue\u00df, \u201cHierarchical verification of two-dimensional high-speed multiplication in PVS: A case study,\u201d in M. Srivas and A. Camilleri (Eds.), Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of Lecture Notes in Computer Science, Palo Alto, CA, Springer-Verlag, pp. 79\u201393, 1996."},{"key":"194807_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/3-540-61474-5_63","volume-title":"Computer-Aided Verification, CAV '96","author":"H. Rue\u00df","year":"1996","unstructured":"H. Rue\u00df, N. Shankar, and M.K. Srivas, \u201cModular verification of SRT division,\u201d in R. Alur and T.A. Henzinger (Eds.), Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, Springer-Verlag, pp. 123\u2013134, 1996."},{"key":"194807_CR29","unstructured":"D.M. Russinoff, \u201cA mechanically checked proof of the correctness of the AMD K5 floating-point square root algorithm,\u201d this Journal."},{"issue":"4","key":"194807_CR30","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1145\/322033.322034","volume":"24","author":"R.E. Shostak","year":"1977","unstructured":"R.E. Shostak, \u201cOn the SUP-INF method for proving Presburger formulas,\u201d Journal of the ACM, Vol. 24,No. 4, pp. 529\u2013543, Oct. 1977.","journal-title":"Journal of the ACM"},{"key":"194807_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods in Computer-Aided Design (FMCAD '96)","year":"1996","unstructured":"M. Srivas and A. Camilleri (Eds.), Formal Methods in Computer-Aided Design (FMCAD '96), volume 1166 of Lecture Notes in Computer Science, Palo Alto, CA, Springer-Verlag, 1996."},{"key":"194807_CR32","unstructured":"Standard for Binary Floating-Point Arithmetic, 1985. ANSI\/IEEE Std 754\u20131985."},{"key":"194807_CR33","unstructured":"Standard for Radix-Independent Floating-Point Arithmetic, 1987. ANSI\/IEEE Std 854\u20131987."},{"key":"194807_CR34","doi-asserted-by":"crossref","unstructured":"G.S. Taylor, \u201cCompatible hardware for division and square root,\u201d in Proceedings of the 5th Symposium on Computer Arithmetic, IEEE Computer Society Press, pp. 127\u2013134, 1981.","DOI":"10.1109\/ARITH.1981.6159293"},{"key":"194807_CR35","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1093\/qjmam\/11.3.364","volume":"3","author":"K.D. Tochter","year":"1958","unstructured":"K.D. Tochter, \u201cTechniques of multiplication and division for automatic binary computers,\u201d Quart. J. Mech. Appl. Match, Vol. 3, pp. 364\u2013384, 1958.","journal-title":"Quart. J. Mech. Appl. Match"},{"key":"194807_CR36","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF01383955","volume":"3","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. 3, pp. 5\u201331, Jan. 1994.","journal-title":"Formal Methods in System Design"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008617612073.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008617612073\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008617612073.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:46:54Z","timestamp":1754369214000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008617612073"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["194807"],"URL":"https:\/\/doi.org\/10.1023\/a:1008617612073","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}