{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:19:32Z","timestamp":1754486372765},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_3","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:13:28Z","timestamp":1269882808000},"page":"8-22","source":"Crossref","is-referenced-by-count":6,"title":["A Proof of Correctness of a Processor Implementing Tomasulo\u2019s Algorithm without a Reorder Buffer"],"prefix":"10.1007","author":[{"given":"Ravi","family":"Hosabettu","sequence":"first","affiliation":[]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[]},{"given":"Mandayam","family":"Srivas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"T. Arons and A. Pnueli. Verifying Tomasulo\u2019s algorithm by refinement. Technical report, Weizmann Institute, 1998.","DOI":"10.1109\/ICVD.1999.745165"},{"key":"3_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-49519-3_24","volume-title":"Formal Methods in Computer-Aided Design, FMCAD\u2019 98","author":"S. Berezin","year":"1998","unstructured":"Sergey Berezin, Armin Biere, Edmund Clarke, and Yunshan Zu. Combining symbolic model checking with uninterpreted functions for out-of-order processor verification. In Ganesh Gopalakrishnan and Phillip Windley, editors, Formal Methods in Computer-Aided Design, FMCAD\u2019 98, volume 1522 of Lecture Notes in Computer Science, pages 369\u2013386, Palo Alto, CA, USA, November 1998. Springer-Verlag."},{"key":"3_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design, FMCAD\u2019 96","author":"C. Barrett","year":"1996","unstructured":"Clark Barrett, David Dill, and Jeremy Levitt. Validity checking for combinations of theories with equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design, FMCAD\u2019 96, volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201, Palo Alto, CA, November 1996. Springer-Verlag."},{"key":"3_CR4","series-title":"Lect Notes Comput Sci","first-page":"203","volume-title":"Theorem Provers in Circuit Design, TPCD\u2019 94","author":"D. Cyrluk","year":"1994","unstructured":"D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Ramayya Kumar and Thomas Kropf, editors, Theorem Provers in Circuit Design, TPCD\u2019 94, volume 910 of Lecture Notes in Computer Science, pages 203\u2013222, Bad Herrenalb, Germany, September 1994. Springer-Verlag."},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare. Proof of correctness of data representations. In Acta Informatica, volume 1, pages 271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"3_CR6","unstructured":"Ravi Hosabettu. The Completion Functions Approach homepage, 1999. At address http:\/\/www.cs.utah.edu\/~hosabett\/cfa.html ."},{"key":"3_CR7","volume-title":"Computer Architecture: A Quantitative Approach","author":"J. L. Hennessy","year":"1990","unstructured":"John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo, CA, 1990."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Thomas Henzinger, Shaz Qadeer, and Sriram Rajamani. You assume, we guarantee: Methodology and case studies. In Hu and Vardi [HV98], pages 440\u2013451.","DOI":"10.1007\/BFb0028765"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Decomposing the proof of correctness of pipelined microprocessors. In Hu and Vardi [HV98], pages 122\u2013134.","DOI":"10.1007\/BFb0028739"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan. Proof of correctness of a processor with reorder buffer using the completion functions approach. 1999. Accepted for publication in the Conference on Computer Aided Verification, Trento, Italy.","DOI":"10.1007\/3-540-48683-6_7"},{"key":"3_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 98","year":"1998","unstructured":"Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, BC, Canada, June\/July 1998. Springer-Verlag."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Ken McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In Hu and Vardi [HV98], pages 110\u2013121.","DOI":"10.1007\/BFb0028738"},{"issue":"2","key":"3_CR13","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"J. Sawada and W. A. Hunt, Jr. Processor verification with precise exceptions and speculative execution. In Hu and Vardi [HV98], pages 135\u2013146.","DOI":"10.1007\/BFb0028740"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:01:36Z","timestamp":1558969296000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}