{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T18:18:07Z","timestamp":1777141087311,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540272311","type":"print"},{"value":"9783540316862","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11513988_2","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:33:28Z","timestamp":1268400808000},"page":"2-4","source":"Crossref","is-referenced-by-count":12,"title":["Validating a Modern Microprocessor"],"prefix":"10.1007","author":[{"given":"Bob","family":"Bentley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems\u00a016, 3 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Colwell, R.P., Brennan, R.: Intel\u2019s Formal Verification Experience on the Willamette Development. In: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics (August 2000)","DOI":"10.1007\/3-540-44659-1_7"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Bentley, B.: Validating the Intel\u00ae Pentium\u00ae 4 Microprocessor. In: Proceedings of the International Conference on Dependable Systems and Networks, June-July (2001)","DOI":"10.1145\/378239.378473"},{"key":"2_CR4","unstructured":"Burns, D.: Pre-Silicon Validation of Hyper-Threading Technology. Intel Technology Journal\u00a06(1) (February 2002)"},{"key":"2_CR5","unstructured":"Kaivola, R., Narasimhan, N.: Verification of Pentium\u00ae4 Multiplier with Symbolic Simulation & Theorem Proving. In: Proceedings of the Design, Automation and Test in Europe Conference (March 2002)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Bentley, B.: High Level Validation of Next-Generation Microprocessors. In: Seventh Annual IEEE International Workshop on High Level Design, Validation and Test (October 2002)","DOI":"10.1109\/HLDVT.2002.1224424"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Schubert, T.: High Level Formal Verification of Next-Generation Microprocessors. In: Proceedings of the 40th Design Automation Conference (June 2003)","DOI":"10.1145\/775833.775834"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11513988_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T23:46:59Z","timestamp":1685490419000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11513988_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540272311","9783540316862"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/11513988_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}