{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:09:42Z","timestamp":1725494982645},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540653882"},{"type":"electronic","value":"9783540493662"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49366-2_3","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T13:48:47Z","timestamp":1194961727000},"page":"22-42","source":"Crossref","is-referenced-by-count":1,"title":["Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover"],"prefix":"10.1007","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[]},{"given":"M.","family":"Subramaniam","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1998,11,30]]},"reference":[{"key":"3_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/3-540-61474-5_62","volume-title":"Proc. Computer Aided Verification, 8th Intl. Conf.","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 Proc. Computer Aided Verification, 8th Intl. Conf. Brunswick, August 1996, Springer LNCS 1102, 111\u2013122."},{"unstructured":"Proc. of the IEEE International Symposium on Computer Arithmetic,, IEEE Computer Society 1995.","key":"3_CR2"},{"unstructured":"Proc. of the IEEE International Symposium on Computer Arithmetic,, IEEE Computer Society 1997.","key":"3_CR3"},{"doi-asserted-by":"crossref","unstructured":"M.P. Heimdahl and N. Leveson, \u201cConsistency and completeness analyses of state-based requirements,\u201d 17th Intl. Conf. on Software Eng., IEEE, 1995.","key":"3_CR4","DOI":"10.1145\/225014.225015"},{"doi-asserted-by":"crossref","unstructured":"C. Heitmeyer, A. Bull, C. Gasarch, B. Labaw, \u201cSCR*: A toolset for specifying and analyzing requirements,\u201d In Proc. of COMPASS\u201995, IEEE 1995.","key":"3_CR5","DOI":"10.21236\/ADA465318"},{"unstructured":"D.N. Hoover and Z. Chen, \u201cTablewise, a decision table tool\u201d, In Proc. of COMPASS\u201995, IEEE 1995.","key":"3_CR6"},{"key":"3_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FMCAD\u201996","author":"P.S. Miner","year":"1996","unstructured":"P.S. Miner and J.F. Leathrum Jr., \u201cVerification of IEEE compliant subtractive division algorithm,\u201d Proc. FMCAD\u201996, LNCS 1166, Palo Alto, CA, 1996."},{"key":"3_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028393","volume-title":"10th Intl. Conf. Theorem Proving in Higher Order Logics","author":"D. Kapur","year":"1997","unstructured":"D. Kapur, \u201cRewriting, decision procedures and lemma speculation for automated hardware verification,\u201d Proc. 10th Intl. Conf. Theorem Proving in Higher Order Logics, LNCS 1275, 1997."},{"unstructured":"D. Kapur and X. Nie, \u201cReasoning about numbers in Tecton,\u201d Proc. 8th Intl. Symp. Methodologies for Intelligent Systems, (ISMIS\u201994), October 1994.","key":"3_CR9"},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of 17th FSTTCS","author":"D. Kapur","year":"1997","unstructured":"D. Kapur, M. Subramaniam \u201cMechanizing Reasoning About Arithmetic Circuits: SRT Division,\u201d In Proc. of 17th FSTTCS, LNCS (eds. Sivakumar and Ramesh), 1997."},{"unstructured":"A.R. Omondi, Computer Arithmetic Systems: Algorithms, Architecture and Imple-mentations, Prentice Hall 1994.","key":"3_CR11"},{"doi-asserted-by":"crossref","unstructured":"K.D. Tocher, \u201cTechniques of multiplication and division for automatic binary com-puters,\u201d Quarterly Journal of Mechanics and Applied Mathematics, 11(3), 1958.","key":"3_CR12","DOI":"10.1093\/qjmam\/11.3.364"},{"doi-asserted-by":"crossref","unstructured":"G.S. Taylor, \u201cCompatible hardware for division and square root,\u201d Proc. 5th IEEE Symp. on Computer Architecture, May 1981.","key":"3_CR13","DOI":"10.1109\/ARITH.1981.6159293"},{"key":"3_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of TACAS","author":"S. Owre","year":"1997","unstructured":"S. Owre, J.R. Rushby, N. Shankar, \u201cIntegration in PVS: Tables, Types, and Model Checking,\u201d Proc. of TACAS,, LNCS 1217, Springer Verlag, April 1997."},{"doi-asserted-by":"crossref","unstructured":"M.D. Ercegovac, T. Lang, \u201cRadix-4 Square Root Without Initial PLA,\u201d IEEE Trans. on Computers, Vol. 39. No. 8, Aug. 1990.","key":"3_CR15","DOI":"10.1109\/12.57040"},{"doi-asserted-by":"crossref","unstructured":"J.H. Zurawski, J.B. Gosling, \u201cDesign of a high speed square root multiply and divide unit\u201d, IEEE Trans. on Computers, vol. C-36, 1987.","key":"3_CR16","DOI":"10.1109\/TC.1987.5009445"},{"unstructured":"D.D. Sarma and D. Matula, \u201cMeasuring the Accuracy of ROM Reciprocal Tables\u201d, IEEE Int. Symp. on Comput. Arithmetic, IEEE Computer Society, 1993.","key":"3_CR17"},{"key":"3_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Computer Aided Verification, 8th Intl. Conf.-CAV\u201996","author":"H. Ruess","year":"1996","unstructured":"H. Ruess, N. Shankar and M.K. Srivas, \u201cModular verification of SRT division,\u201d Proc. Computer Aided Verification, 8th Intl. Conf.-CAV\u201996, New Brunswick, 1996, Springer LNCS 1102 (eds. Alur and Henzinger)."},{"doi-asserted-by":"crossref","unstructured":"J.E. Robertson, \u201cA new class of digital division methods,\u201d IRE Trans. on Electronic Computers, 1958, 218\u2013222.","key":"3_CR19","DOI":"10.1109\/TEC.1958.5222579"},{"key":"3_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 9th (CADE)","author":"H. Zhang","year":"1988","unstructured":"H. Zhang, D. Kapur, and M.S. Krishnamoorthy, \u201cdA mechanizable induction principle for equational specifications,\u201d Proc. 9th (CADE), Springer LNCS 310, 1988."}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science ASIAN 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49366-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T06:17:08Z","timestamp":1556950628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49366-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540653882","9783540493662"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-49366-2_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}