{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:14:29Z","timestamp":1773656069818,"version":"3.50.1"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2002,3]]},"DOI":"10.1023\/a:1014170513439","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T14:45:40Z","timestamp":1041086740000},"page":"159-186","source":"Crossref","is-referenced-by-count":12,"title":["Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function"],"prefix":"10.1007","volume":"20","author":[{"given":"Sergey","family":"Berezin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yunshan","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"393305_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-49519-3_24","volume-title":"FMCAD'98","author":"S. Berezin","year":"1998","unstructured":"S. Berezin, A. Biere, E. Clarke, and Y. Zhu, \u201cCombining symbolic model checking with uninterpreted functions for out-of-order processor verification,\u201d in FMCAD'98, Lecture Notes in Computer Science, Vol. 1522, Springer-Verlag, Berlin, 1998, pp. 369\u2013386."},{"key":"393305_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"TACAS'99","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu, \u201cSymbolic model checking without BDDs,\u201d in TACAS'99, Lecture Notes in Computer Science, Vol. 1579, Springer-Verlag, Amsterdam, The Netherlands, 1999."},{"key":"393305_CR3","unstructured":"R.E. Bryan, S. German, and M.N. Velev, \u201cProcessor verification using efficient reductions of the logic of uninterpreted functions to propositional logic,\u201d Technical Report, Carnegie Mellon University, 1999.Available as http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/1999\/CMU-CS-99-115.ps."},{"issue":"8","key":"393305_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. 35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"393305_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification (CAV'94)","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch and D.L. Dill, \u201cAutomatic verification of pipelined microprocessor control,\u201d in D.L. Dill (Ed.), Computer Aided Verification (CAV'94), Lecture Notes in Computer Science, Vol. 18, Springer-Verlag, Berlin, 1994."},{"key":"393305_CR6","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, \u201cDesign and synthesis of synchronization skeletons using branching time temporal logic,\u201d in Proceedings of the IBM Workshop on Logics of Programs, Springer-Verlag, Berlin, 1981, pp. 52\u201371."},{"issue":"2","key":"393305_CR7","doi-asserted-by":"crossref","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, \u201cAutomatic verification of finite-state concurrent systems using temporal logic specifications,\u201d ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, pp. 244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"393305_CR8","volume-title":"Computer Aided Verification (CAV'98)>","author":"Computer Aided Verification","year":"1998","unstructured":"Computer Aided Verification (CAV'98), Lecture Notes in Computer Science, Vol. 1427, Springer-Verlag, Berlin, June 1998."},{"key":"393305_CR9","volume-title":"Computer Aided Verification (CAV'99)","author":"Computer Aided Verification","year":"1999","unstructured":"Computer Aided Verification (CAV'99), Lecture Notes in Computer Science, Vol. 1633, Springer-Verlag, Berlin, July 1999."},{"key":"393305_CR10","volume-title":"CHARME'97","author":"W. Damm","year":"1997","unstructured":"W. Damm and A. Pnueli, \u201cVerifying out-of-order executions,\u201d in D. Probst (Ed.), CHARME'97, Chapman &; Hall, London, 1997."},{"issue":"2","key":"393305_CR11","first-page":"9","volume":"9","author":"L. Gwennap","year":"1995","unstructured":"L. Gwennap, \u201cIntel's P6 uses decoupled superscalar design,\u201d Microprocessor Report, Vol. 9, No. 2, pp. 9\u201315, 1995.","journal-title":"Microprocessor Report"},{"key":"393305_CR12","volume-title":"Computer Architecture: A Quantitative Approach","author":"J. Hennessy","year":"1996","unstructured":"J. Hennessy and D. Patterson, Computer Architecture: A Quantitative Approach, Morgan Kaufmann, San Mateo, CA, 1996."},{"key":"393305_CR13","volume-title":"Computer Aided Verification (CAV'95)","author":"R. Hojati","year":"1995","unstructured":"R. Hojati and R.K. Brayton, \u201cAutomatic datapath abstraction of hardware systems,\u201d in Computer Aided Verification (CAV'95), Springer-Verlag, Berlin, 1995."},{"key":"393305_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/BFb0028739","volume-title":"Computer Aided Verification (CAV'98)","author":"R. Hosabettu","year":"1998","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan, \u201cDecomposing the proof of correctness of pipelined microprocessors,\u201d in Computer Aided Verification (CAV'98), Lecture Notes in Computer Science, Vol. 1427, Springer-Verlag, Berlin, June 1998, pp. 122\u2013134."},{"key":"393305_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification (CAV'99)","author":"R. Hosabettu","year":"1999","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan, \u201cProof of correctness of a processor with reorder buffer using the completion function approach,\u201d in Computer Aided Verification (CAV'99), Lecture Notes in Computer Science, Vol. 1633, Springer-Verlag, Berlin, July 1999."},{"issue":"1\/2","key":"393305_CR16","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"C.N. Ip and D.L. Dill, \u201cBetter verification through symmetry,\u201d Formal Methods in System Design, Vol. 9, No. 1\/2, pp. 41\u201375, 1996.","journal-title":"Formal Methods in System Design"},{"key":"393305_CR17","volume-title":"The Implementation of Functional Programming Languages","author":"S.L.P. Jones","year":"1987","unstructured":"S.L.P. Jones, The Implementation of Functional Programming Languages, Prentice-Hall, Englewood Cliffs, NJ, 1987."},{"key":"393305_CR18","volume-title":"The Architecture of Symbolic Computers","author":"P.M. Kogge","year":"1991","unstructured":"P.M. Kogge, The Architecture of Symbolic Computers, McGraw-Hill, New York, 1991."},{"key":"393305_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic Publishers, Dordrecht, 1993."},{"key":"393305_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification (CAV'98)","author":"K.L. McMillan","year":"1998","unstructured":"K.L. McMillan, \u201cVerification of an implementation of tomasulo's algorithm by compositional model checking,\u201d in Computer Aided Verification (CAV'98), Lecture Notes in Computer Science, Vol. 1427, Springer-Verlag, Berlin, June 1998."},{"key":"393305_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification (CAV'98)","author":"K. Sajid","year":"1998","unstructured":"K. Sajid, A. Goel, H. Zhou, A. Aziz, and V. Singhal, \u201cBDD based procedures for a theory of equality with uninterpreted functions,\u201d in Computer Aided Verification (CAV'98), Lecture Notes in Computer Science, Vol. 1427, Springer-Verlag, Berlin, June 1998."},{"key":"393305_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification (CAV'98)","author":"J. Sawada","year":"1998","unstructured":"J. Sawada and W.A. Hunt, \u201cProcessor verification with precise exceptions and speculative execution,\u201d in Computer Aided Verification (CAV'98), Lecture Notes in Computer Science, Vol. 1427, Springer-Verlag, Berlin, June 1998."},{"key":"393305_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification (CAV'98)","author":"J.U. Skakkeb\u00e6k","year":"1998","unstructured":"J.U. Skakkeb\u00e6k, R.B. Jones, and D.L. Dill, \u201cFormal verification of out-of-order execution using incremental flushing,\u201d in Computer Aided Verification (CAV'98), Lecture Notes in Computer Science, Vol. 1427, Springer-Verlag, Berlin, June 1998."},{"key":"393305_CR24","series-title":"Lecture Notes in Computer Science","first-page":"37","volume-title":"Correct Hardware Design and Verification Methods (CHARME'99)","author":"M.N. Velev","year":"1999","unstructured":"M.N. Velev and R.E. Bryant, \u201cSuperscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions,\u201d in Correct Hardware Design and Verification Methods (CHARME'99), Lecture Notes in Computer Science, Vol. 1703, Springer-Verlag, Berlin, 1999, pp. 37\u201353."},{"key":"393305_CR25","unstructured":"D.H.D. Warren, \u201cAn abstract prolog instruction set,\u201d Technical Note 309, SRI International, 1983."},{"key":"393305_CR26","first-page":"184","volume-title":"Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages (POPL'86)","author":"P. Wolper","year":"1986","unstructured":"P. Wolper, \u201cExpressing interesting properties of programs in propositional temporal logic,\u201d in Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages (POPL'86), ACM, New York, 1986, pp. 184\u2013193."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1014170513439.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1014170513439\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1014170513439.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T20:08:01Z","timestamp":1754424481000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1014170513439"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["393305"],"URL":"https:\/\/doi.org\/10.1023\/a:1014170513439","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}