{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,15]],"date-time":"2025-07-15T03:45:31Z","timestamp":1752551131511,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425410"},{"type":"electronic","value":"9783540447986"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1007\/3-540-44798-9_33","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T17:16:15Z","timestamp":1178212575000},"page":"433-448","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["A Framework for Microprocessor Correctness Statements"],"prefix":"10.1007","author":[{"given":"Mark D.","family":"Aagaard","sequence":"first","affiliation":[]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[]},{"given":"Nancy A.","family":"Day","sequence":"additional","affiliation":[]},{"given":"Robert B.","family":"Jones","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"issue":"82","key":"33_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"2","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 2(82):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"T. Arons and A. Pnueli. Verifying Tomasulo\u2019s algorithm by refinement. In Int\u2019l Conference on VLSI Design, pp 92\u201399, 1999.","DOI":"10.1109\/ICVD.1999.745165"},{"key":"33_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1007\/3-540-46419-0_33","volume-title":"TACAS","author":"T. Arons","year":"2000","unstructured":"T. Arons and A. Pnueli. A comparison of two verification methods for speculative instruction execution with exceptions. In TACAS, vol 1785 of LNCS, pp 487\u2013502. Springer, 2000."},{"issue":"3","key":"33_CR4","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/40.768501","volume":"19","author":"Arvind","year":"1999","unstructured":"Arvind and X. Shen. Using term rewriting systems to design and verify processors. IEEE Micro, 19(3):36\u201346, 1999.","journal-title":"IEEE Micro"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"D. Beatty and R. Bryant. Formally verifying a microprocessor using a simulation methodology. In DAC, pp 596\u2013602, 1994.","DOI":"10.1145\/196244.196575"},{"key":"33_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-49519-3_24","volume-title":"FMCAD","author":"S. Berezin","year":"1998","unstructured":"S. Berezin, A. Biere, E. Clarke, and Y. Zhu. Combining symbolic model checking with uninterpreted functions for out-of-order processor verification. In FMCAD, vol 1522 of LNCS, pp 369\u2013386. Springer, 1998."},{"key":"33_CR7","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, vol 818 of LNCS, pp 68\u201380. Springer, 1994."},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"S. Bose and A. Fisher. Verifying pipelined hardware using symbolic logic simulation. In ICCD, pp 217\u2013221, 1989.","DOI":"10.1109\/ICCD.1989.63359"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"R. Bryant, S. German, and M. Velev. Processor verification using efficient decision procedures for a logic of uninterpreted functions. In TABLEAUX, vol 1617 of LNAI, pp 1\u201313. Springer, June 1999.","DOI":"10.1007\/3-540-48754-9_1"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"J. Burch. Techniques for verifying superscalar microprocessors. In DAC, pp 552\u2013557, 1996.","DOI":"10.1145\/240518.240623"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"W. Damm and A. Pnueli. Verifying out-of-order executions. In CHARME, pp 23\u201347. Chapman and Hall, 1997.","DOI":"10.1007\/978-0-387-35190-2_3"},{"key":"33_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-49254-2_5","volume-title":"Prospects for Hardware Foundations","author":"A. Fox","year":"1998","unstructured":"A. Fox and N. Harman. An algebraic model of correctness for superscaler microprocessors. In Prospects for Hardware Foundations, vol 1546 of LNCS, pp 138\u2013183. Springer, 1998."},{"key":"33_CR13","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, vol 1855 of LNCS, pp 521\u2013537. Springer, 2000."},{"key":"33_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/BFb0028765","volume-title":"CAV","author":"T. Henzinger","year":"1998","unstructured":"T. Henzinger, S. Qadeer, and S. Rajamani. You assume, we guarantee: Methodology and case studies. In CAV, vol 1427 of LNCS, pp 440\u2013451. Springer, 1998."},{"key":"33_CR15","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, vol 1427 of LNCS, pp 122\u2013134. Springer, 1998."},{"key":"33_CR16","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 processorwith reorder buffer using the completion functions approach. In CAV, vol 1633 of LNCS, pp 47\u201359. Springer, 1999."},{"key":"33_CR17","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, vol 1522 of LNCS, pp 2\u201317. Springer, 1998."},{"key":"33_CR18","series-title":"Lect Notes Comput Sci","first-page":"161","volume-title":"FMCAD","author":"P. Manolios","year":"2000","unstructured":"P. Manolios. Correctness of pipelined machines. In FMCAD, vol 1954 of LNCS, pp 161\u2013178. Springer, 2000."},{"key":"33_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"CAV","author":"K. McMillan","year":"1998","unstructured":"K. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In CAV, vol 1427 of LNCS, pp 110\u2013121. Springer, 1998."},{"key":"33_CR20","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proc. of 2nd Int\u2019l Joint Conf. on Artificial Intelligence, pp 481\u2013489. The British Comp. Soc., 1971."},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"R. Nalumasu and G. Gopalakrishnan. Deriving efficient cache coherence protocols through refinement. In Formal Methods for Parallel Programming: Theory and Applications (FMPPTA\u201998), 1998.","DOI":"10.1007\/3-540-64359-1_748"},{"key":"33_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-49519-3_23","volume-title":"FMCAD","author":"A. Pnueli","year":"1998","unstructured":"A. Pnueli and T. Arons. Verification of data-insensitive circuits: An in-order-retirement case study. In FMCAD, vol 1522 of LNCS, pp 351\u2013368. Springer, 1998."},{"key":"33_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/3-540-61474-5_78","volume-title":"CAV","author":"S. Park","year":"1996","unstructured":"S. Park and D. Dill. Protocol verification by aggregation of distributed transactions. In CAV, vol 1102 of LNCS, pp 300\u2013310. Springer, 1996."},{"key":"33_CR24","first-page":"282","volume-title":"Int\u2019l Conf. on VLSI Design","author":"V. Patankar","year":"1999","unstructured":"V Patankar, A. Jain, and R. E. Bryant. Formal verification of an ARM processor. In Int\u2019l Conf. on VLSI Design, pp 282\u2013287. IEEE; New York, NY, January 1999."},{"key":"33_CR25","unstructured":"S. Qadeer. Algorithms and Methodology for Scalable Model Checking. PhD thesis, Elec. Eng. and Comp. Sci., University of California at Berkeley, 1999."},{"key":"33_CR26","unstructured":"A97]_X. Shen and Arvind. A methodology for designing correct cache coherence protocols for DSM systems. Technical Report CSG Memo 398 (A), MIT, June 1997."},{"key":"33_CR27","doi-asserted-by":"crossref","unstructured":"M. Srivas and M. Bickford. Formal verification of a pipelined microprocessor. IEEE Trans. on Software Engineering, pp 52\u201364, September 1990.","DOI":"10.1109\/52.57892"},{"key":"33_CR28","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, vol 1254 of LNCS, pp 364\u2013375. Springer, 1997."},{"key":"33_CR29","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, vol 1427 of LNCS, pp 135\u2013146. Springer, 1998."},{"key":"33_CR30","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, vol 1703 of LNCS, pp 313\u2013316. Springer, 1999."},{"key":"33_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/BFb0028737","volume-title":"CAV","author":"J. Skakkeb\u00e6k","year":"1998","unstructured":"J. Skakkeb\u00e6k, R. Jones, and D. Dill. Formal verification of out-of-order execution using incremental flushing. In CAV, vol 1427 of LNCS, pp 98\u2013109. Springer, 1998."},{"key":"33_CR32","doi-asserted-by":"crossref","unstructured":"M. K. Srivas and S. P. Miller. Applying formal verification to a commercial microprocessor. In CHDL, pp 493\u2013502, August 1995.","DOI":"10.1109\/ASPDAC.1995.486361"},{"key":"33_CR33","doi-asserted-by":"crossref","unstructured":"P. Windley and M. Coe. A correctness model for pipelined microprocessors. In Theorem Provers in Circuit Design, pp 32\u201351. Springer, 1994.","DOI":"10.1007\/3-540-59047-1_41"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44798-9_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:57:14Z","timestamp":1736989034000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44798-9_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425410","9783540447986"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-44798-9_33","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"24 August 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}