{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:04Z","timestamp":1725664924484},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602750"},{"type":"electronic","value":"9783540447849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60275-5_68","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:06:09Z","timestamp":1330279569000},"page":"229-244","source":"Crossref","is-referenced-by-count":0,"title":["Formal verification of serial pipeline multipliers"],"prefix":"10.1007","author":[{"given":"Jang Dae","family":"Kim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shiu-Kai","family":"Chin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"3","key":"16_CR1","first-page":"413","volume":"AU-16","author":"H. S. McDonald","year":"1968","unstructured":"Henry S. McDonald, Leland B. Jackson, James F. Kaiser, \u201cAn approach to the implementation of digital filters,\u201d IEEE Trans. on Audio and Electroacoustics, AU-16(3):413\u2013421, Sept 1968.","journal-title":"IEEE Trans. on Audio and Electroacoustics"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"R. F. Lyon, \u201cTwo's complement pipeline multipliers,\u201d IEEE Transactions on Communications, pages 418\u2013425, April 1976.","DOI":"10.1109\/TCOM.1976.1093315"},{"key":"16_CR3","unstructured":"Shiu-Kai Chin, Juin-Yeu Lu, \u201cThe mechanical verification and synthesis of parameterized serial\/parallel multiplier,\u201d Technical Report 9140, CASE Center, Syracuse University, 1991."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Shiu-Kai Chin, \u201cVerified Functions for Generating Signed-Binary Arithmetic Hardware,\u201d IEEE Trans. Computer-Aided Design, pages 1529\u20131558, December 1992.","DOI":"10.1109\/43.180266"},{"key":"16_CR5","unstructured":"Amir Pnueli, Zohar Manna, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, 1992."},{"key":"16_CR6","unstructured":"Michael J.C. Gordon, \u201cWhy higher-order logic is a good formalism for specifying and verifying hardware,\u201d In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design, pages 153\u2013177. Elsevier Scientific Publishers, 1986."},{"key":"16_CR7","volume-title":"Modelling bit vectors in HOL: the word library","author":"W. Wong","year":"1994","unstructured":"Wai Wong, \u201cModelling bit vectors in HOL: the word library,\u201d Proc. of 6th Intl. HOL Users Group Workshop 1993, Vancouver, B.C, Canada, August 1993, Springer-Verlag, New York, 1994."},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science 780","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J. Y. Lu","year":"1994","unstructured":"J. Y. Lu, S. K. Chin, \u201cLinking HOL to a VLSI CAD system,\u201d Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science 780, Springer-Verlag, Berlin Heidelberg 1994."},{"key":"16_CR9","unstructured":"Mentor Graphics Inc., GDT Led, Lx Standard Cell, Explorer Lsim V.5.3 users manuals, San Jose, CA, 1990."},{"key":"16_CR10","unstructured":"Mentor Graphics Inc., Explorer AutoCells Users Guide, San Jose, CA, 1990."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60275-5_68.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:57:20Z","timestamp":1605646640000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_68"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_68","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}