{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:58:19Z","timestamp":1754485099902},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028737","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"98-109","source":"Crossref","is-referenced-by-count":16,"title":["Formal verification of out-of-order execution using incremental flushing"],"prefix":"10.1007","author":[{"given":"Jens U.","family":"Skakkeb\u00e6k","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert B.","family":"Jones","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,18]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. L. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In FMCAD '96, volume 1166 of LNCS, pages 187-201, Stanford, CA, USA, November 1996. Springer-Verlag.","DOI":"10.1007\/BFb0031808"},{"key":"12_CR2","series-title":"DAC","first-page":"552","volume-title":"Techniques for verifying superscalar microprocessors","author":"J. R. Burch","year":"1996","unstructured":"J. R. Burch. Techniques for verifying superscalar microprocessors. In DAC, pages 552\u2013557, Las Vegas, Nevada, USA, June 1996. ACM Press."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of microprocessor control. In David L. Dill, editor, CAV, volume 818 of LNCS, pages 68-80, Stanford, California, USA, June 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"W. Damm and A. Pnueli. Verifying out-of-order executions. In H.F. Li and D.K. Probst, editors, CHARME '97, pages 23\u201347, Montreal, Canada, October 1997. Chapman & Hall.","DOI":"10.1007\/978-0-387-35190-2_3"},{"key":"12_CR5","unstructured":"J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1990."},{"key":"12_CR6","doi-asserted-by":"crossref","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 Californaia, Berkeley, CA 94720, 1998.","DOI":"10.1007\/BFb0028765"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"R. B. Jones, D. L. Dill, and J. R. Burch. Efficient validity checking for processor verification. In ICCAD'95, November 1995.","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"R. B. Jones, C.-J. H. Seger, and D. L. Dill. Self-consistency checking. In FMCAD '96, volume 1166 of LNCS, pages 159-171, Stanford, CA, USA, November 1996. Springer-Verlag.","DOI":"10.1007\/BFb0031806"},{"key":"12_CR9","series-title":"LNCS","first-page":"361","volume-title":"Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness.","author":"B. Jonsson","year":"1989","unstructured":"B. Jonsson. On decomposing and refining specifications of distributed systems. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness., volume 430 of LNCS, pages 361\u2013385, Mook, The Netherlands, May-June 1989. Springer-Verlag."},{"key":"12_CR10","series-title":"DIMACS, Series in Discrete Mathematics and Theoretical Computer Science","first-page":"59","volume-title":"Partial Order Methods in Verification","author":"S. Katz","year":"1996","unstructured":"S. Katz. Refinement with global equivalence proofs in temporal logic. In D. A. Peled, V R. Pratt, and G. J. Holzmann, editors, Partial Order Methods in Verification, volume 29 of DIMACS, Series in Discrete Mathematics and Theoretical Computer Science, pages 59\u201378, Princeton, NJ, USA, 1996. Amer. Math. Society."},{"key":"12_CR11","unstructured":"K. McMillan. Verification of an implementation of Tomasulo's algorithm by compositional model checking. Appears in this volume."},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, CAV '96, volume 1102 of LNCS, pages 411\u2013414, New Brunswick, NJ, July\/Aug 1996. Springer-Verlag.","DOI":"10.1007\/3-540-61474-5_91"},{"key":"12_CR13","unstructured":"J. Sawada and W. A. Hunt. Processor verification with precise exceptions and speculative execution. Appears in this volume."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"J. Sawada and W. A. Hunt. Trace table based approach for pipelined microprocessor verification. In Orna Grumberg, editor, CAV '97, volume 1254 of LNCS, pages 364\u2013375, Haifa, Israel, June 1997. Springer-Verlag.","DOI":"10.1007\/3-540-63166-6_36"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"P J. Windley and J. R. Burch. Mechanically checking a lemma used in an automatic verification tool. In FMCAD'96, pages 362\u2013376, November 1996.","DOI":"10.1007\/BFb0031821"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028737","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:23:56Z","timestamp":1586593436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028737"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0028737","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}