{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:28:21Z","timestamp":1690975701502},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,7,7]],"date-time":"2009-07-07T00:00:00Z","timestamp":1246924800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,8]]},"DOI":"10.1007\/s10703-009-0080-2","type":"journal-article","created":{"date-parts":[[2009,7,6]],"date-time":"2009-07-06T14:51:22Z","timestamp":1246891882000},"page":"56-72","source":"Crossref","is-referenced-by-count":5,"title":["Word level bitwidth reduction for unbounded hardware model checking"],"prefix":"10.1007","volume":"35","author":[{"given":"Per","family":"Bjesse","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,7,7]]},"reference":[{"key":"80_CR1","unstructured":"Baumgartner J, Gloekler T, Shanmugam D, Seigler R, Huben GV, Mony H, Roessler P, Ramanandray B (2006) Enabling large-scale pervasive logic verification through multi-algorithmic formal reasoning. In: Proc of the formal methods in CAD conf, 2006"},{"key":"80_CR2","doi-asserted-by":"crossref","unstructured":"Bjesse P (2008) A practical approach to word level model checking of industrial netlists. In: Proc of the computer aided verification conf, 2008","DOI":"10.1007\/978-3-540-70545-1_43"},{"key":"80_CR3","doi-asserted-by":"crossref","unstructured":"Bryant R, German S, Velev M (1999) Exploiting positive equality in a logic of equality with uninterpreted functions. In: Proc of the computer aided verification conf, 1999","DOI":"10.1007\/3-540-48683-6_40"},{"key":"80_CR4","doi-asserted-by":"crossref","unstructured":"Bryant R, Lahiri S, Seshia S (2002) Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Proc of the computer aided verification conf, 2002","DOI":"10.1007\/3-540-45657-0_7"},{"key":"80_CR5","doi-asserted-by":"crossref","unstructured":"Galler B, Fischer M (1964) An improved equivalence algorithm. Commun ACM (May)","DOI":"10.1145\/364099.364331"},{"key":"80_CR6","doi-asserted-by":"crossref","unstructured":"Hojati R, Brayton R (1995) Automatic datapath abstraction in hardware systems. In: Proc of the computer aided verification conf, 1995","DOI":"10.1007\/3-540-60045-0_43"},{"key":"80_CR7","unstructured":"Ip CN, Dill DL (1996) Better verification through symmetry. Form Methods Syst Des (August)"},{"key":"80_CR8","unstructured":"Johannesen P (2002) Speeding up hardware verification by automated data path scaling. PhD thesis, Christian-Albrechts-Universit\u00e4t zu Kiel"},{"key":"80_CR9","doi-asserted-by":"crossref","unstructured":"Manolios P, Srinivasan S, Vroon D (2007) BAT: The bit-level analysis tool. In: Proc of the computer aided verification conf, 2007","DOI":"10.1007\/978-3-540-73368-3_35"},{"key":"80_CR10","unstructured":"Peh L-S, Dally W (2001) A delay model and speculative architecture for pipelined routers. In: Proc intl symposium on high-performance computer architecture, 2001"},{"key":"80_CR11","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/S0890-5401(02)93175-5","volume":"178","author":"A Pnueli","year":"2002","unstructured":"Pnueli A, Rodeh Y, Strichmann O, Siegel M (2002) The small model property: how small can it be? Inf Comput 178:279\u2013293","journal-title":"Inf Comput"},{"key":"80_CR12","unstructured":"Pugh W (1999) Skip lists: a probabilistic alternative to balanced trees. Commun ACM (June)"},{"key":"80_CR13","unstructured":"Ranise S, Tinelli C (2006) Satisfiability modulo theories. Trends and controversies. IEEE Intell Syst Mag (December)"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0080-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0080-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0080-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:51Z","timestamp":1559253951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0080-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,7,7]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["80"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0080-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,7,7]]}}}