{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:06:11Z","timestamp":1761645971472},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"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":[[2000]]},"DOI":"10.1007\/3-540-40922-x_11","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T04:41:36Z","timestamp":1196311296000},"page":"181-198","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Correctness of Pipelined Machines"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"B. Brock, M. Kaufmann, and J. S. Moore. ACL2 theorems about commercial microprocessors. In M. Srivas and A. Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD\u201996), pages 275\u2013293. Springer-Verlag, 1996.","DOI":"10.1007\/BFb0031816"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"M. Browne, E. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59, 1988.","DOI":"10.21236\/ADA188620"},{"key":"11_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Computer-Aided Verification-CAV\u2019 99","author":"R. E. Bryant","year":"1999","unstructured":"R. E. Bryant, S. German, and M. N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification-CAV\u2019 99, volume 1633 of LNCS, pages 470\u2013482. Springer-Verlag, 1999."},{"key":"11_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification (CAV\u2019 94)","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill. Automatic veri_cation of pipelined microprocessor control. In Computer-Aided Verification (CAV\u2019 94), volume 818 of LNCS, pages pp68-80. Springer-Verlag, 1994."},{"key":"11_CR5","unstructured":"D. Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI, Dec. 1993."},{"key":"11_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/3-540-48683-6_20","volume-title":"Computer-Aided Verification CAV\u2019 99","author":"T. A. Henzinger","year":"1999","unstructured":"T. A. Henzinger, S. Qadeer, and S. K. Rajamani. Assume-guarantee refinement between different time scales. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification CAV\u2019 99, volume 1633 of LNCS, pages 208\u2013221. Springer-Verlag, 19"},{"key":"11_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/3-540-48153-2_3","volume-title":"A proof of correctness of a processor implementing Tomasulo\u2019s algorithm without a reorder buffer","author":"R. Hosabettu","year":"1999","unstructured":"R. Hosabettu, G. Gopalakrishnan, and M. Srivas. A proof of correctness of a processor implementing Tomasulo\u2019s algorithm without a reorder buffer. In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods, 10th IFIP WG10.5 Advanced Research Working Conference, (CHARME\u2019 99), volume 1703 of LNCS, pages 8\u201322. Springer-Verlag, 1999."},{"key":"11_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification CAV\u2019 98","author":"R. Hosabettu","year":"1998","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Decomposing the proof of correctness of a pileplined microprocessors. In A. J. Hu and M. Vardi, editors, Computer-Aided Verification CAV\u2019 98, volume 1427 of LNCS. Springer-Verlag, 19"},{"key":"11_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification CAV\u2019 99","author":"R. Hosabettu","year":"1999","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan. Proof of correctness of a processor with reorder buffer using the completion functions approach. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification CAV\u2019 99, volume 1633 of LNCS. Springer-Verlag, 19"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, P. Manolios, and J. S. Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, June 2000.","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Press, July 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"11_CR12","unstructured":"M. Kaufmann and J. S. Moore. ACL2 homepage. See URL \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\n                    \n                  ."},{"key":"11_CR13","unstructured":"M. Kaufmann and J. S. Moore. Structured theory development for a mechanized logic. Journal of Automated Reasoning, 2000. To appear, See URL \n                    http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/acl2-papers.html#Foundations\n                    \n                  ."},{"key":"11_CR14","unstructured":"P. Manolios. Homepage of Panagiotis Manolios, 2000. See URL \n                    http:\/\/www.cs.utexas.edu\/users\/pete\n                    \n                  ."},{"key":"11_CR15","unstructured":"P. Manolios. Well-founded equivalence bisimulation. Technical report, Department of Computer Sciences, University of Texas at Austin, 2000. In preparation."},{"key":"11_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-48683-6_32","volume-title":"Computer-Aided Verification CAV\u2019 99","author":"P. Manolios","year":"1999","unstructured":"P. Manolios, K. Namjoshi, and R. Sumners. Linking theorem proving and model-checking with well-founded bisimulation. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification CAV\u2019 99, volume 1633 of LNCS, pages 369\u2013379. Springer-Verlag, 19"},{"key":"11_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification (CAV\u2019 98)","author":"K. L. McMillan","year":"1998","unstructured":"K. L. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV\u2019 98), volume 1427 of LNCS, pages 110\u2013121. Springer-Verlag, 1998."},{"key":"11_CR18","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, 1990."},{"key":"11_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"A simple characterization of stuttering bisimulation","author":"K. S. Namjoshi","year":"1997","unstructured":"K. S. Namjoshi. A simple characterization of stuttering bisimulation. In 17th Conference on Foundations of Software Technology and Theoretical Computer Science,volume 1346 of LNCS, pages 284\u2013296, 1997."},{"key":"11_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"D. Park. Concurrency and automata on in_nite sequences. In Theoretical Computer Science, volume 104 of LNCS, pages 167\u2013183. Springer-Verlag, 1981."},{"key":"11_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-48683-6_39","volume-title":"Computer-Aided Verification CAV\u2019 99","author":"A. Pnueli","year":"1999","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domain instantiations. In N. Halbwachs and D. Peled, editors, Computer-Aided Verification CAV\u2019 99, volume 1633 of LNCS, pages 455\u2013469. Springer-Verlag, 19"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"J. Sawada. Formal Verification of an Advanced Pipelined Machine. PhD thesis, University of Texas at Austin, Dec. 1999. See URL \n                    http:\/\/www.cs.utexas.edu\/users\/sawada\/dissertation\/\n                    \n                  .","DOI":"10.1007\/978-1-4757-3188-0_9"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"J. Sawada. Verification of a simple pipelined machine model. In M. Kaufmann, P. Manolios, and J. S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, pages 137\u2013150. Kluwer Academic Press, 2000.","DOI":"10.1007\/978-1-4757-3188-0_9"},{"key":"11_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/3-540-63166-6_36","volume-title":"Computer Aided Verification (CAV\u2019 97)","author":"J. Sawada","year":"1997","unstructured":"J. Sawada and W. A. Hunt, Jr. Trace table based approach for pipelined micro-processor verification. In Computer Aided Verification (CAV\u2019 97), volume 1254 of LNCS, pages 364\u2013375. Springer-Verlag, 1997."},{"key":"11_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"Computer Aided Verification (CAV\u2019 98)","author":"J. Sawada","year":"1998","unstructured":"J. Sawada and W. A. Hunt, Jr. Processor verification with precise exceptions and speculative execution. In A. J. Hu and M. Y. Vardi, editors, Computer Aided Verification (CAV\u2019 98), volume 1427 of LNCS, pages 135\u2013146. Springer-Verlag, 1998."},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"M. Srivas and M. Bickford. Formal verification of a pipelined microprocessor. IEEE Software, pages 52\u201364, Sept. 1990.","DOI":"10.1109\/52.57892"},{"key":"11_CR27","unstructured":"M. K. Srivas and S. P. Miller. Formal verification of an avionics microprocessor. Technical Report CSL-95-04, SRI International, 1995."},{"key":"11_CR28","series-title":"Lect Notes Comput Sci","first-page":"33","volume-title":"Theorem Provers in Circuit Design","author":"P. J. Windley","year":"1994","unstructured":"P. J. Windley and M. L. Coe. A correctness model for pipelined microprocessors. In Theorem Provers in Circuit Design, volume 901 of LNCS, pages 33\u201352. Springer-Verlag, 1994."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T07:45:14Z","timestamp":1580283914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}