{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:22:15Z","timestamp":1754482935545},"publisher-location":"Berlin, Heidelberg","reference-count":11,"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\/bfb0031806","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"159-171","source":"Crossref","is-referenced-by-count":16,"title":["Self-consistency checking"],"prefix":"10.1007","author":[{"given":"Robert B.","family":"Jones","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carl-Johan H.","family":"Seger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"V. Bhagwati and S. Devadas. Automatic verification of pipelined microprocessors. In 31st ACM\/IEEE Design Automation Conference, 1994.","DOI":"10.1145\/196244.196577"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of microprocessor control. In Computer Aided Verification. 6th International Conference, 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"J. R. Burch. Techniques for verifying superscalar microprocessors. In 33rd ACM\/IEEE Design Automation Conference, 1996.","DOI":"10.1145\/240518.240623"},{"key":"11_CR4","unstructured":"D. Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, December 1993."},{"key":"11_CR5","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF00121125","volume":"1","author":"A. Gupta","year":"1992","unstructured":"A. Gupta. Formal hardware verification methods: A survey. Formal Methods in System Design, 1:5\u201392, 1992.","journal-title":"Formal Methods in System Design"},{"key":"11_CR6","unstructured":"J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1990."},{"key":"11_CR7","unstructured":"W. A. Hunt, Jr. FM8501: A verified microprocessor. Technical Report 47, University of Texas at Austin, Institute for Computing Science, December 1985."},{"key":"11_CR8","unstructured":"C. H. Seger. Voss: A formal hardware verification system user's guide. Technical Report 93\u201345, Department of Computer Science, Univerisity of British Columbia, 1993."},{"key":"11_CR9","unstructured":"J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning. Using transformations and verification in circuit design. Technical Report 78, DEC Systems Research Center, September 1991."},{"key":"11_CR10","first-page":"18","volume":"840","author":"R. Wilson","year":"1995","unstructured":"R. Wilson. Verification feels strain. Electronic Engineering Times, (840):18\u201322, March 1995.","journal-title":"Electronic Engineering Times"},{"issue":"1","key":"11_CR11","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/12.368009","volume":"44","author":"P. J. Windley","year":"1995","unstructured":"P. J. Windley. Formal modeling and verification of microprocessors. IEEE Transactions on Computers, 44(1):54\u201372, January 1995.","journal-title":"IEEE Transactions on Computers"}],"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\/BFb0031806","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:49:41Z","timestamp":1586612981000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031806"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0031806","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}