{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:20:55Z","timestamp":1747592455975},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662020"},{"type":"electronic","value":"9783540486831"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_9","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"72-83","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists"],"prefix":"10.1007","author":[{"given":"Jason","family":"Baumgartner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tamir","family":"Heyman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vigyan","family":"Singhal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"S. Mador-Haim and L. Fix. Input Elimination and Abstraction in Model Checking. In G. Gopalakrishnan and P. Windley, editor, Proc. Conf. on Formal Methods in Computer-Aided Design, volume 1522, pages 304\u2013320. Springer, November 1998.","key":"9_CR1","DOI":"10.1007\/3-540-49519-3_20"},{"unstructured":"K. Nowka and T. Galambos. Circuit Design Techniques for a Gigahertz Integer Microprocessor. In Proc. Intl. Conf. on Computer Design, October 1998.","key":"9_CR2"},{"issue":"1","key":"9_CR3","first-page":"41","volume":"1","author":"C. E. Leiserson","year":"1983","unstructured":"C. E. Leiserson and J. B. Saxe. Optimizing Synchronous Systems. Journal of VLSI and Computer Systems, 1(1):41\u201367, Spring 1983.","journal-title":"Journal of VLSI and Computer Systems"},{"doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and A. Landver. RuleBase: an Industry-Oriented Formal Verification Tool. In Proc. Design Automation Conf., June 1996.","key":"9_CR4","DOI":"10.1145\/240518.240642"},{"key":"9_CR5","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, New York, 1989."},{"unstructured":"Z. Kohavi. Switching and Finite Automata Theory. Computer Science Series. McGraw-Hill Book Company, 1970.","key":"9_CR6"},{"issue":"3","key":"9_CR7","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D. E. Long. Module Checking and Modular Verification. ACM Transactions on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"9_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","key":"9_CR9","DOI":"10.1007\/978-1-4615-3190-6"},{"unstructured":"A. J. Hu, G. York, and D. L. Dill. New Techniques for Efficient Verification with Implicitly Conjoined BDDs. In Proc. Design Automation Conf., June 1994.","key":"9_CR10"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T06:05:26Z","timestamp":1586153126000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}