{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:29:04Z","timestamp":1754483344193},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_2","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T10:37:12Z","timestamp":1192876632000},"page":"2-17","source":"Crossref","is-referenced-by-count":13,"title":["Reducing Manual Abstraction in Formal Verification of Out- of- Order Execution"],"prefix":"10.1007","author":[{"given":"Robert B.","family":"Jones","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens U.","family":"Skakkeb\u00c6k","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":[[2002,5,17]]},"reference":[{"unstructured":"S. Berezin, A. Biere, E. Clarke, and Y. Zhu. Combining symbolic model checking with uninterpreted functions for out-of-order processor verification. Appears in this volume.","key":"2_CR1"},{"doi-asserted-by":"crossref","unstructured":"J. R. Burch. Techniques for verifying superscalar microprocessors. In 33rd ACM\/IEEE Design Automation Conference, pages 552\u2013557, Las Vegas, Nevada, USA, June 1996. ACM Press.","key":"2_CR2","DOI":"10.1145\/240518.240623"},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification. 6th International Conference","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of microprocessor control. In David L. Dill, editor, Computer Aided Verification. 6th International Conference, volume 818 of LNCS, pages 68\u201380, Stanford, California, USA, June 1994. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"Werner Damm and Amir Pnueli. Verifying out-of-order executions. In Hon F. li and David K. Probst, editors, Advances in Hardware Design and Verification: IFIP WG10.5 Internation al Conference on Correct Hardware Design and Verification Methods (CHARME), pages 23\u201347, Montreal, Canada, October 1997. Chapman & Hall.","key":"2_CR4","DOI":"10.1007\/978-0-387-35190-2_3"},{"unstructured":"J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1990.","key":"2_CR5"},{"key":"2_CR6","volume-title":"Technical report","author":"T. A. Henzinger","year":"1998","unstructured":"T. A. Henzinger, S. Qadeer, and S. K. Rajamani. You assume, we guarantee: Methodology and case studies. Technical report, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, 1998."},{"key":"2_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0028739","volume-title":"Computer Aided Verification (CAV\u201998)","author":"R. Hosabettu","year":"1998","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Decomposing the proof of correctness of pipelined microprocessors. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV\u201998), volume 1427 of Lecture Notes in Computer Science, pages 122\u2013134, Vancouver, Canada, June-July 1998. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"R. B. Jones, D. L. Dill, and J. R. Burch. Efficient validity checking for processor verification. In Proceedings: IEEE International Conference on Computer-Aided Design (ICCAD), November 1995.","key":"2_CR8","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"2_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification (CAV\u201998)","author":"K. McMillan","year":"1998","unstructured":"K. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV\u201998), volume 1427 of Lecture Notes in Computer Science, pages 110\u2013121, Vancouver, Canada, June\u2013July 1998. Springer-Verlag."},{"key":"2_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-63166-6_36","volume-title":"Computer-Aided Verification, CAV\u2019 97","author":"J. Sawada","year":"1997","unstructured":"J. Sawada and W. A. Hunt. Trace table based approach for pipelined microprocessor verification. In Orna Grumberg, editor, Computer-Aided Verification, CAV\u2019 97, volume 1254 of Lecture Notes in Computer Science, pages 364\u2013375, Haifa, Israel, June 1997. Springer-Verlag."},{"key":"2_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"Computer Aided Verification (CAV\u201998)","author":"J. Sawada","year":"1998","unstructured":"J. Sawada and W. A. Hunt. Processor Verification with precise exceptions and speculative execution. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV\u201998), volume 1427 of Lecture Notes in Computer Science, pages 135\u2013146, Vancouver, Canada, June-July 1998. Springer-Verlag."},{"key":"2_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/BFb0028737","volume-title":"Computer Aided Verification (CAV\u201998)","author":"J. U. Skakkeb\u00c6k","year":"1998","unstructured":"J. U. Skakkeb\u00c6k, R. B. Jones, and D. L. Dill. Formal Verification of out-of-order execution using incremental flushing. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV\u201998), volume 1427 of Lecture Notes in Computer Science, pages 98\u2013109, Vancouver, Canada, June\u2013July 1998. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"P. J. Windley and J. R. Burch. Mechanically checking a lemma used in an automatic Verification tool. In Proceedings: International Conference on Formal Methods in Computer-Aided Design, pages 362\u2013376, November 1996.","key":"2_CR13","DOI":"10.1007\/BFb0031821"}],"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\/3-540-49519-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T21:59:09Z","timestamp":1556920749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}