{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:52:32Z","timestamp":1754488352689},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540619376"},{"type":"electronic","value":"9783540495673"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0031801","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"79-93","source":"Crossref","is-referenced-by-count":2,"title":["Hierarchical verification of two-dimensional high-speed multiplication in PVS: A case study"],"prefix":"10.1007","author":[{"given":"Harald","family":"Rue\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"M.D. Aagaard and C.J.H. Seger. The Formal Verification of a Pipelined Double-Precision IEEE Floating-Point Multiplier. In Proc. of ICCAD'95, pages 7\u201310. IEEE Computer Science Press, 1995.","DOI":"10.1109\/ICCAD.1995.479878"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and Y.A. Chen. Verification of Arithmetic Circuits with Binary Moment Diagrams. Technical Report CMU-CS-94-160, School of Computer Science, Carnegie Mellon University, 1994.","DOI":"10.21236\/ADA281028"},{"key":"6_CR3","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":"6_CR4","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":"6_CR5","unstructured":"Y.A. Chen and R.E. Bryant. ACV: An Arithmetic Circuit Verifier. 1995."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, S.M. German, and X. Zhao. Verifying the SRT Division Algorithm using Theorem Proving Techniques. In R. Alur and T.A. Henzinger, editors, CAV'96, number 1102 in Lecture Notes in Computer Science, pages 111\u2013122. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_62"},{"issue":"2","key":"6_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. Verified Functions for Generating Signed-Binary Arithmetic Hardware. IEEE Transactions on Computer-Aided Design, 11(2):1529\u20131558, December 1992.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"D. Cyrluk, S. Rajan, N. Shankar, and M. Srivas. Effective Theorem Proving for Hardware Verification. In R. Kumar and Th. Kropf, editors, Theorem Provers in Circuit Design, number 901 in Lecture Notes in Computer Science, 1994.","DOI":"10.1007\/3-540-59047-1_50"},{"issue":"9","key":"6_CR9","doi-asserted-by":"crossref","first-page":"949","DOI":"10.1109\/32.58783","volume":"16","author":"F.K. Hanna","year":"1990","unstructured":"F.K. Hanna, N. Daeche, and M. Longley. Specification and Verification Using Dependent Types. IEEE Transactions on Software Engineering, 16(9):949\u2013964, September 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR10","unstructured":"I. Koren. Computer Arithmetic Algorithms. Prentice-Hall, 1993."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"D. Kapur and M. Subramaniam. Mechanically Verifying a Family of Multiplier Circuits. In R. Alur and T.A. Henzinger, editors, CAV'96, number 1102 in LNCS, pages 135\u2013146. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_64"},{"key":"6_CR12","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":"6_CR13","doi-asserted-by":"crossref","unstructured":"P.S. Miner and J.F. Leathrum. Verification of IEEE Compliant Subtractive Division Algorithms. 1996. FMCAD'96, This Volume.","DOI":"10.1007\/BFb0031800"},{"issue":"2","key":"6_CR14","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. 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":"6_CR15","doi-asserted-by":"crossref","unstructured":"H. Rue\u00df, M. Srivas, and N. Shankar. Modular Verification of SRT Division. In R. Alur and T.A. Henzinger, editors, CAV'96, number 1102 in Lecture Notes in Computer Science, pages 123\u2013134. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_63"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031801","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:49:57Z","timestamp":1586612997000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031801"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0031801","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}