{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:18:46Z","timestamp":1754482726446},"publisher-location":"Berlin, Heidelberg","reference-count":19,"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_63","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:40:52Z","timestamp":1330292452000},"page":"123-134","source":"Crossref","is-referenced-by-count":11,"title":["Modular verification of SRT division"],"prefix":"10.1007","author":[{"given":"H.","family":"Rue\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. K.","family":"Srivas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"issue":"10","key":"11_CR1","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":"11_CR2","series-title":"15213","volume-title":"Technical Report CMU-CS-94-160","author":"R.E. Bryant","year":"1994","unstructured":"R.E. Bryant. Verification of Arithmetic Functions with Binary Moment Diagrams. Technical Report CMU-CS-94-160, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, 1994."},{"key":"11_CR3","series-title":"15213","volume-title":"Technical Report CMU-CS-95-140","author":"R.E. Bryant","year":"1995","unstructured":"R.E. Bryant. Bit-Level Analysis of an SRT Divider Circuit. Technical Report CMU-CS-95-140, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, April 1995."},{"key":"11_CR4","unstructured":"E.M. Clarke and S.M. German. Personal Communication, 1995."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, S.M. German, and X. Zhao. Verifying the SRT Division Algorithm using Theorem Proving Techniques. Submitted to CAV'96, 1996.","DOI":"10.1007\/3-540-61474-5_62"},{"key":"11_CR6","series-title":"15213","volume-title":"Technical Report CMU-CS-95-161","author":"E.M. Clarke","year":"1995","unstructured":"E.M. Clarke and X. Zhao. Word Level Symbolic Model Checking: A New approach for Verifying Arithmetic Circuits. Technical Report CMU-CS-95-161, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, April 1995."},{"key":"11_CR7","unstructured":"S.M. German. Towards Automatic Verification of Arithmetic Hardware. Lecture notes, March 1995."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"M. Leeser and J. O'Leary. Verification of a Subtractive Radix-2 Square Root Algorithm and Implementation. In Proc. of ICCD'95, pages 526\u2013531. IEEE Computer Society Press, 1995.","DOI":"10.1109\/ICCD.1995.528918"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"O.L. McSorley. High-speed Arithmetic in Binary Computers. In Proc. of IRE, pages 67\u201391, 1961.","DOI":"10.1109\/JRPROC.1961.287779"},{"key":"11_CR10","volume-title":"NASA Technical Memorandum 110167","author":"P.S. Miner","year":"1995","unstructured":"P.S. Miner. Defining the IEEE-854 floating-point standard in PVS. NASA Technical Memorandum 110167, NASA Langley Research Center, Hampton, VA, June 1995."},{"key":"11_CR11","series-title":"94305-2140","volume-title":"Technical Report CSL-TR-94-647","author":"S.F. Oberman","year":"1994","unstructured":"S.F. Oberman and M.J. Flynn. Design Issues in Floating-Point Division. Technical Report CSL-TR-94-647, Dept. of Computer Science, Stanford University, Stanford, CA 94305-2140, December 1994."},{"key":"11_CR12","volume-title":"Technical Report CSL-95-12","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, and N. Shankar. Analyzing Tabular and State-Transition Specification in PVS. Technical Report CSL-95-12, Computer Science Laboratory, SRI International, Menlo Park CA 94025 USA, June 1995."},{"issue":"2","key":"11_CR13","doi-asserted-by":"publisher","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. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR14","unstructured":"D. L. Parnas. Using mathematical models in the inspection of critical softwa re. In Michael G. Hinchey and Jonathan P. Bowen, editors, Applications of Formal Methods, International Series in Computer Science, chapter 2, pages 17\u201331. Prentice Hall, 1995."},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"V. Pratt. Anatomy of the Pentium Bug. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, TAPSOFT'95: Theory and Practice of Software Development, number 915 in Lecture Notes in Computer Science, pages 97\u2013107. Springer Verlag, May 1995.","DOI":"10.1007\/3-540-59293-8_189"},{"key":"11_CR16","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. A new Class of Digital Division Methods. In IRE Trans. on Electron. Computers, volume EC-7, pages 218\u2013222, 1958.","journal-title":"IRE Trans. on Electron. Computers"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"G.S. Taylor. Compatible Hardware For Division and Square Root. In Proceedings of the 5th Symposium on Computer Arithmetic, pages 127\u2013134. IEEE Computer Society Press, 1981.","DOI":"10.1109\/ARITH.1981.6159293"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"K.D. Tochter. Techniques of Multiplication and Division for Automatic Bin ary Computers. In Quart. J. Mech. Appl. Match, volume Part 3, pages 364\u2013384, 1958.","DOI":"10.1093\/qjmam\/11.3.364"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01383955","volume":"3","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, 3:5\u201331, January 1994.","journal-title":"Formal Methods in System Design"}],"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_63.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:06:38Z","timestamp":1605647198000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_63"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_63","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}