{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:59:46Z","timestamp":1754488786060},"publisher-location":"Berlin, Heidelberg","reference-count":24,"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_24","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T06:37:12Z","timestamp":1192862232000},"page":"369-386","source":"Crossref","is-referenced-by-count":16,"title":["Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification"],"prefix":"10.1007","author":[{"given":"Sergey","family":"Berezin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yunshan","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"issue":"8","key":"24_CR1","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"doi-asserted-by":"crossref","unstructured":"J. R. Burch. Techniques for verifying superscalar microprocessors. In 33rd Design Automation Conference (DAC\u201996), pages 552\u2013557, 1996.","key":"24_CR2","DOI":"10.1145\/240518.240623"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201994","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In D. L. Dill, editor, CAV\u201994, volume 818 of LNCS. Springer-Verlag, 1994."},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","first-page":"52","volume-title":"Proceedings of the IBM Workshop on Logics of Programs","author":"E. Clarke","year":"1981","unstructured":"E. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the IBM Workshop on Logics of Programs, volume 131 of LNCS, pages 52\u201371. Springer-Verlag, 1981."},{"issue":"2","key":"24_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0016951","volume-title":"Symmetry and induction in model checking","author":"E. M. Clarke","year":"1995","unstructured":"E. M. Clarke and S. Jha. Symmetry and induction in model checking. Number 1000 in LNCS. Springer-Verlag, 1995."},{"doi-asserted-by":"crossref","unstructured":"W. Damm and A. Pnueli. Verifying out-of-order executions. In D. Probst, editor, CHARME\u201997. Chapman & Hall, 1997. To appear.","key":"24_CR8","DOI":"10.1007\/978-0-387-35190-2_3"},{"issue":"2","key":"24_CR9","first-page":"9","volume":"9","author":"L. Gwennap","year":"1995","unstructured":"L. Gwennap. Intel\u2019s P6 uses decoupled superscalar design. Microprocessor Report, 9(2):9\u201315, 1995.","journal-title":"Microprocessor Report"},{"unstructured":"J. Hennessy and D. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers, 1996.","key":"24_CR10"},{"doi-asserted-by":"crossref","unstructured":"R. Hojati and R. K. Brayton. Automatic datapath abstraction of hardware systems. In CAV\u201995. Springer-Verlag, 1995.","key":"24_CR11","DOI":"10.1007\/3-540-60045-0_43"},{"key":"24_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/BFb0028739","volume-title":"CAV\u201998","author":"R. Hosabettu","year":"1998","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Decomposing the proof of correctness of pipelined microprocessors. In Moshe Y. Vardi, editors. CAV\u201998, number 1427 in LNCS, 1998 Hu and Vardi [13], pages 122\u2013134."},{"key":"24_CR13","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","year":"1998","unstructured":"Alan J. Hu and Moshe Y. Vardi, editors. CAV\u201998, number 1427 in LNCS, 1998."},{"unstructured":"S. L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987.","key":"24_CR14"},{"unstructured":"Peter M. Kogge. The Architecture of Symbolic Computers. McGraw-Hill, 1991.","key":"24_CR15"},{"doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","key":"24_CR16","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"24_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"CAV\u201998","author":"K.L. McMillan","year":"1998","unstructured":"K. L.McMillan. Verification of an implementation of tomasulo\u2019s algorithm by compositional model checking. In Moshe Y. Vardi, editors. CAV\u201998, number 1427 in LNCS, 1998 Hu and Vardi [13], pages 110\u2013121."},{"key":"24_CR18","series-title":"Lect Notes Comput Sci","first-page":"244","volume-title":"CAV\u201998","author":"K. Sajid","year":"1998","unstructured":"K. Sajid, A. Goel, H. Zhou, A. Aziz, and V. Singhal. BDD based procedures for a theory of equality with uninterpreted functions. In Moshe Y. Vardi, editors. CAV\u201998, number 1427 in LNCS, 1998 Hu and Vardi [13], pages 244\u2013255."},{"key":"24_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"CAV\u201998","author":"J. Sawada","year":"1998","unstructured":"J. Sawada and W. A. Hunt. Processor verification with precise exceptions and speculative execution. In Moshe Y. Vardi, editors. CAV\u201998, number 1427 in LNCS, 1998 Hu and Vardi [13], pages 135\u2013146."},{"unstructured":"N. Shankar, S. Owre, and J. M. Rushby. PVS Tutorial. Computer Science Laboratory, SRI International, 1993.","key":"24_CR20"},{"key":"24_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/BFb0028737","volume-title":"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 Moshe Y. Vardi, editors. CAV\u201998, number 1427 in LNCS, 1998 Hu and Vardi [13], pages 98\u2013109."},{"doi-asserted-by":"crossref","unstructured":"M. N. Velev and R. E. Bryant. Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking. 1998. Submitted for publication.","key":"24_CR22","DOI":"10.1007\/3-540-49519-3_3"},{"unstructured":"D. H. D. Warren. An abstract prolog instruction set. Tech. Note 309, SRI, 1983.","key":"24_CR23"},{"doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proceedings of the 13th annual ACM Symposium on Principles of Programming Languages (POPL\u201986), pages 184\u2013193. ACM, 1986.","key":"24_CR24","DOI":"10.1145\/512644.512661"}],"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_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:59:05Z","timestamp":1556906345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}