{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:43Z","timestamp":1725664183029},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:37:30Z","timestamp":1330277850000},"page":"98-113","source":"Crossref","is-referenced-by-count":31,"title":["Automatic datapath abstraction in hardware systems"],"prefix":"10.1007","author":[{"given":"Ramin","family":"Hojati","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"8","key":"9_CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph Based Algorithms for Boolean Function Manipulation\u201d, IEEE Trans. on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Trans. on Computers"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"J. Burch, D. Dill, \u201cAutomated Verification of Pipelined Micro-processors\u201d, Computer-Aided Verification, 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"D. Cyrluk, P. Narendran, \u201cGround Temporal Logic: A Logic for Hardware Verification\u201d, Computer-Aided Verification, 1994.","DOI":"10.1007\/3-540-58179-0_59"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"R. Hojati, R. K. Brayton, \u201cAn Environment for Formal Verification Based On Symbolic Computations\u201d, Journal of Formal Methods, 1995.","DOI":"10.1007\/BF01383967"},{"key":"9_CR5","unstructured":"R. Hojati, S. Krishnan, R. K. Brayton, \u201cHeuristic Algorithms for Early Quantification and Partial Product Minimization\u201d, ERL Memorandum M94\/11, March 1994, UC Berkeley."},{"key":"9_CR6","unstructured":"R. Hojati, R. Mueller-Thuns, P. Lowenstein, R. K. Brayton, \u201cAutomatic Verification of Memory System Using Language Containment and Abstraction\u201d, to be submitted to CHDL 95."},{"key":"9_CR7","unstructured":"C. N. Ip, D. Dill, \u201cBetter Verification through Symmetry\u201d, Symp. on Computer Hardware Description Languages and Their Application, 1993."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"E. Macii, B. Plessier, F. Somenzi, \u201cVerification of Systems Containing Counters\u201d, IEEE\/ACM International Conference on Computer-Aided Design, 1992.","DOI":"10.1109\/ICCAD.1992.279378"},{"key":"9_CR9","unstructured":"R. P. Kurshan, \u201cAutomata-Theoretic Verification of Coordinating Processes\u201d, UC Berkeley notes, 1992."},{"key":"9_CR10","unstructured":"N. Shankar, S. Owre, J. M. Rushby, \u201cThe PVS Specification and Verification System\u201d, SRI International, 1993."},{"issue":"No.2","key":"9_CR11","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. E. Shostak","year":"1979","unstructured":"R. E. Shostak, \u201cA Practical Decision Procedure for Arithmetic With Function Symbols\u201d, JACM Volume 26, No. 2, April 1979, pp. 351\u2013360.","journal-title":"JACM"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"P. Wolper, \u201cExpressing Interesting Properties of Programs\u201d, 13th Annual ACM Symp. on Principles of Prog. Languages, 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:28:50Z","timestamp":1605648530000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}