{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:47:51Z","timestamp":1725551271248},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_8","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:55:19Z","timestamp":1269885319000},"page":"123-141","source":"Crossref","is-referenced-by-count":14,"title":["Relating Multi-step and Single-Step Microprocessor Correctness Statements"],"prefix":"10.1007","author":[{"given":"Mark D.","family":"Aagaard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meng","family":"Lou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/3-540-44798-9_33","volume-title":"CHARME","author":"M. D. Aagaard","year":"2001","unstructured":"M. D. Aagaard, B. Cook, N. A. Day, and R. B. Jones. A framework for microprocessor correctness statements. In CHARME, volume 2144 of LNCS, pages 433\u2013448. Springer, 2001."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, B. Cook, N. A. Day, and R. B. Jones. A framework for superscalar microprocessor correctness statements, 2002. To appear in Software Tools for Technology Transfer.","DOI":"10.1007\/s10009-002-0087-0"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"T. Arons and A. Pnueli. Verifying Tomasulo\u2019s algorithm by refinement. In Int\u2019l Conf. on VLSI Design, pages 92\u201399. IEEE Comp. Soc. Press, 1999.","DOI":"10.1109\/ICVD.1999.745165"},{"issue":"2","key":"8_CR4","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1023\/A:1014170513439","volume":"20","author":"S. Berezin","year":"2002","unstructured":"S. Berezin, E. Clarke, A. Biere, and Y. Zhu. Verification of out-of-order processor designs using model checking and a light-weight completion function. Formal Methods in System Design, 20(2): 159\u2013186, March 2002.","journal-title":"Formal Methods in System Design"},{"key":"8_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"CAV","author":"J. Burch","year":"1994","unstructured":"J. Burch and D. Dill. Automatic verification of pipelined microprocessor control. In CAV, volume 818 of LNCS, pages 68\u201380. Springer, 1994."},{"key":"8_CR6","unstructured":"N. A. Day, M. D. Aagaard, and M. Lou. A mechanized theory for microprocessor correctness statements. Technical Report 2002-11, U. of Waterloo, Dept. of Comp. Sci., 2002."},{"issue":"4","key":"8_CR7","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/PL00003936","volume":"12","author":"A. Fox","year":"2000","unstructured":"A. Fox and N. Harman. Algebraic models of correctness for microprocessors. Formal Aspects in Computing, 12(4):298\u2013312, 2000.","journal-title":"Formal Aspects in Computing"},{"key":"8_CR8","unstructured":"M. Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"8_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/10722167_39","volume-title":"CAV","author":"R. Hosabettu","year":"2000","unstructured":"R. Hosabettu, G. Gopalakrishnan, and M. Srivas. Verifying advanced microarchitectures that support speculation and exceptions. In CAV, volume 1855 of LNCS, pages 521\u2013537. Springer, 2000."},{"key":"8_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/BFb0028739","volume-title":"CAV","author":"R. Hosabettu","year":"1998","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Decomposing the proof of correctness of pipelined microprocessors. In CAV, volume 1427 of LNCS, pages 122\u2013134. Springer, 1998."},{"key":"8_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/3-540-48683-6_7","volume-title":"CAV","author":"R. Hosabettu","year":"1999","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Proof of correctness of a processor with reorder buffer using the completion functions approach. In CAV, volume 1633 of LNCS, pages 47\u201359. Springer, 1999."},{"key":"8_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/3-540-48153-2_3","volume-title":"CHARME","author":"R. Hosabettu","year":"1999","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Proof of correctness of a processor without reorder buffer using the completion functions approach. In CHARME, volume 1703 of LNCS, pages 8\u201322. Springer, 1999."},{"key":"8_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-49519-3_2","volume-title":"FMCAD","author":"R. Jones","year":"1998","unstructured":"R. Jones, J. Skakkeb\u00e6k, and D. Dill. Reducing manual abstraction in formal verification of out-of-order execution. In FMCAD, volume 1522 of LNCS, pages 2\u201317. Springer, 1998."},{"issue":"2","key":"8_CR14","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1023\/A:1014118529369","volume":"20","author":"R. B. Jones","year":"2002","unstructured":"R. B. Jones, J. U. Skakkeb\u00e6k,, and D. L. Dill. Formal verification of out-of-order execution using incremental flushing. Formal Methods in System Design, 20(2):39\u201358, March 2002.","journal-title":"Formal Methods in System Design"},{"key":"8_CR15","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Joint Conference on Artificial Intelligence, pages 481\u2013489. British Computer Society, 1971."},{"key":"8_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-63166-6_36","volume-title":"CAV","author":"J. Sawada","year":"1997","unstructured":"J. Sawada and W. Hunt. Trace table based approach for pipelined microprocessor verification. In CAV, volume 1254 of LNCS, pages 364\u2013375. Springer, 1997."},{"key":"8_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"CAV","author":"J. Sawada","year":"1998","unstructured":"J. Sawada and W. Hunt. Processor verification with precise exceptions and speculative execution. In CAV, volume 1427 of LNCS, pages 135\u2013146. Springer, 1998."},{"key":"8_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3-540-48153-2_23","volume-title":"CHARME","author":"J. Sawada","year":"1999","unstructured":"J. Sawada and W. Hunt. Results of the verification of a complex pipelined machine model. In CHARME, volume 1703 of LNCS, pages 313\u2013316. Springer, 1999."}],"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-36126-X_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T04:28:35Z","timestamp":1635136115000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}