{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:26Z","timestamp":1725484286053},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540431596"},{"type":"electronic","value":"9783540456452"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45645-7_7","type":"book-chapter","created":{"date-parts":[[2007,5,29]],"date-time":"2007-05-29T02:24:22Z","timestamp":1180405462000},"page":"128-151","source":"Crossref","is-referenced-by-count":11,"title":["Verifying a Simple Pipelined Microprocessor Using Maude"],"prefix":"10.1007","author":[{"given":"N. A.","family":"Harman","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,1,29]]},"reference":[{"key":"7_CR1","unstructured":"G Birtwistle and B Graham. Verifying SECD in HOL. In J Staunstrup, editor, Formal Methods for VLSI Design, pages 129\u2013177. North-Holland, 1990."},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"J Burch. Techniques for verifying superscalar microprocessors. In Design Automation Conference, 1996.","DOI":"10.1145\/240518.240623"},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Proceedings of the 6th International Conference, CAV\u201994: Computer-Aided Verification","author":"J. Burch","year":"1994","unstructured":"J Burch and D Dill. Automatic Verification of pipelined microprocessor control. In D Dill, editor, Proceedings of the 6th International Conference, CAV\u201994: Computer-Aided Verification, pages 68\u201380. Lecture Notes in Computer Science 818, Springer-Verlag, 1994."},{"key":"7_CR4","unstructured":"M Clavel, F Dur\u00e1n, S Eker, P Lincoln, N MartfOliet, J Meseguer, and J Quesada. Maude: specification and programming in rewriting logic. Technical report, Computer Science Laboratory, SRI International, 1999."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"A Cohn. A proof of correctness of the Viper microprocessor: the first levels. In G Birtwistle and P A Subrahmanyam, editors, VLSI specification, Verification and Synthesis, pages 27\u201372. Kluwer Academic Publishers, 1987.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"7_CR6","unstructured":"B Cook, J Launchbury, and J Matthews. Specifying superscalar microprocessors in Hawk. In M Sheeran, editor, Workshop on Formal Methods for Hardware (Marstrand, Sweden), 1998."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"D Cyrluk, J Rushby, and M Srivas. Systematic formal Verification of interpreters. In IEEE International Conference on Formal Engineering Methods (ICFEM\u201997, pages 140\u2013149, 1997.","DOI":"10.1109\/ICFEM.1997.630421"},{"key":"7_CR8","unstructured":"A C J Fox. Algebraic Representation of Advanced Microprocessors. PhD thesis, Department of Computer Science, University of Wales Swansea, 1998."},{"key":"7_CR9","unstructured":"A C J Fox. Algebraic Techniques for Verifying Microprocessors in HOL. Computer Laboratory Report 512, University of Cambridge, 2001."},{"key":"7_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0031820","volume-title":"Formal Methods in Computer-Aided Design","author":"A. C. J. Fox","year":"1996","unstructured":"A C J Fox and N A Harman. An algebraic model of correctness for superscalar microprocessors. In Formal Methods in Computer-Aided Design, pages 346\u2013361. Lecture Notes in Computer Science 1166, Springer-Verlag, 1996."},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/PL00003936","volume":"12","author":"A. C. J. Fox","year":"2000","unstructured":"A C J Fox and N A Harman. Algebraic models of correctness for microprocessors. Formal Aspects of Computer Science, 12:298\u2013312, 2000.","journal-title":"Formal Aspects of Computer Science"},{"key":"7_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-49254-2_5","volume-title":"Prospects for Hardware Foundations","author":"A. C. J. Fox","year":"1998","unstructured":"A C J Fox and N A Harman. Algebraic models of superscalar microprocessor implementations: A case study. In B M\u00f6ller and J V Tucker, editors, Prospects for Hardware Foundations, pages 138\u2013183. Lecture Notes in Computer Science 1546, Springer-Verlag, 1998."},{"key":"7_CR13","unstructured":"A C J Fox and N A Harman. Algebraic models of temporal abstraction for initialised iterated state systems: An abstract pipelined case study. Technical Report CSR 21-98, University of Wales Swansea, 1998, submitted to the Journal of Algebraic and Logic Programming."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"B Graham. The SECD Microprocessor: a Verification Case Study. Kluwer, 1992.","DOI":"10.1007\/978-1-4615-3576-8"},{"key":"7_CR15","unstructured":"M J C Gordon and T F Melham. Introduction to HOL. Cambridge University Press, 1993."},{"key":"7_CR16","unstructured":"N A Harman. Correctness and Verification of hardware systems using Maude. Technical Report Computer Science Report, University of Wales Swansea, 2000."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"N A Harman and J V Tucker. The formal specification of a digital correlator I: Abstract user specification. In K McEvoy and J V Tucker, editors, Theoretical Foundations for VLSI Design, pages 161\u2013262. Cambridge University Press Tracts in Theoretical Computer Science 10, 1990.","DOI":"10.1017\/CBO9780511569838.008"},{"key":"7_CR18","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s002360050051","volume":"33","author":"N. A. Harman","year":"1996","unstructured":"N A Harman and J V Tucker. Algebraic models of microprocessors: Architecture and organisation. Acta Informatica, 33:421\u2013456, 1996.","journal-title":"Acta Informatica"},{"key":"7_CR19","unstructured":"N A Harman and J V Tucker. Algebraic models of microprocessors: the Verification of a simple computer. In V Stavridou, editor, Proceedings of the 1995 IMA Conference on Mathematics for Dependable Systems. Oxford University Press, 1997."},{"key":"7_CR20","unstructured":"J L Hennessy and D A Patterson. Computer Architecture: A Quantative Approach. Morgan Kaufman, 1996."},{"key":"7_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0028739","volume-title":"Computer Aided Verification: 10th International Conference","author":"R. Hosabettu","year":"1998","unstructured":"R Hosabettu, M Srivas, and G Gopalakrishnan. Decomposing the proof of correctness of pipelined microprocessors. In A J Hu and M Y Vardi, editors, Computer Aided Verification: 10th International Conference, pages 122\u2013134. Springer-Verlag, Lecture Notes in Computer Science 1427, 1998."},{"key":"7_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"Computer Aided Verification: 10th International Conference","author":"J. Sawada","year":"1998","unstructured":"J Sawada W A Hunt. Processor Verification with precise exceptions and speculative execution. In A J Hu and M Y Vardi, editors, Computer Aided Verification: 10th International Conference, pages 135\u2013147. Springer-Verlag, Lecture Notes in Computer Science 1427, 1998."},{"key":"7_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-49519-3_2","volume-title":"Formal Methods in Computer-Aided Design, FMCAD 98","author":"R. B. Jones","year":"1998","unstructured":"R B Jones, J U Skakkeb\u00e6k, and D Dill. Reducing manual abstraction in formal Verification of out-of-order execution. In G Gopalakrishnan and P Windley, editors, Formal Methods in Computer-Aided Design, FMCAD 98, pages 2\u201317. Springer-Verlag, Lecture Notes in Computer Science 1522, 1998."},{"key":"7_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/BFb0028737","volume-title":"Computer Aided Verification: 10th International Conference","author":"J. U. Skakkeb\u00e6k","year":"1998","unstructured":"J U Skakkeb\u00e6k, R B Jones, and D Dill. Formal Verification of out-of-order execution using incremental ushing. In A J Hu and M Y Vardi, editors, Computer Aided Verification: 10th International Conference, pages 98\u2013109. Springer-Verlag, Lecture Notes in Computer Science 1427, 1998."},{"key":"7_CR25","unstructured":"S Krstic, B Cook, J Launchbury, and J Matthews. A correctness proof of a speculative, superscalar, out-of-order, renaming microarchitecture. Technical report, Oregon Graduate Institute, 1998."},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"F Dur\u00e1n M Clavel, S Eker, and J Meseguer. Building equational proving tools by reection in rewriting logic. In K Futatsugi, A T Nakagawa and T Tamai, editors, CAFE: An Industrial-Strength Algebraic Formal Method, pages 1\u201331, Elsevier, 2000.","DOI":"10.1016\/B978-044450556-9\/50061-7"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"K Meinke and J V Tucker. Universal algebra. In T S E Maibaum S Abramsky, D Gabbay, editor, Handbook of Logic in Computer Science, pages 189\u2013411. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537359.003.0003"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"S Miller and M Srivas. Formal Verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods. In Proceedings of WIFT 95, Boca Raton, 1995.","DOI":"10.1109\/WIFT.1995.515475"},{"key":"7_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/3-540-59047-1_53","volume-title":"A tutorial on using PVS","author":"S. Owre","year":"1995","unstructured":"S Owre, J Rushby, N Shankar, and M Srivas. A tutorial on using PVS. In Proceedings of TPCD 94, pages 258\u2013279. Lecture Notes in Computer Science 901, Springer-Verlag, 1994."},{"key":"7_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/3-540-63475-4_4","volume-title":"Formal Hardware Verification","author":"M. Srivas","year":"1997","unstructured":"M Srivas, H Rue\u03b2, and D Cyrluk. Hardware Verification using PVS. In T Kropf, editor, Formal Hardware Verification, pages 156\u2013205. Springer-Verlag, Lecture Notes in Computer Science 1287, 1997."},{"key":"7_CR31","unstructured":"K Stephenson. An Algebraic Approach to Syntax, Semantics and Compilation. PhD thesis, University of Wales Swansea Computer Science Department, 1996."},{"key":"7_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49254-2_7","volume-title":"Prospects for Hardware Foundations","author":"K. Stephenson","year":"1998","unstructured":"K Stephenson. Algebraic specification of the Java virtual machine. In B M\u00f6ller and J V Tucker, editors, Prospects for Hardware Foundations. Lecture Notes in Computer Science 1546, Springer-Verlag, 1998."},{"key":"7_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/BFb0031821","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Windley","year":"1996","unstructured":"P Windley and J Burch. Mechanically checking a lemma used in an automatic Verification tool. In A Camilleri M Srivas, editor, Formal Methods in Computer-Aided Design, pages 362\u2013376. Lecture Notes in Computer Science 1166, Springer-Verlag, 1996."},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"P Windley and M Coe. A correctness model for pipelined microprocessors. In Proceedings of the 2nd Conference on Theorem Provers in Circuit Design, 1994.","DOI":"10.1007\/3-540-59047-1_41"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"M Wirsing. Algebraic specification. In J van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 675\u2013788. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50018-4"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45645-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,14]],"date-time":"2024-02-14T15:51:43Z","timestamp":1707925903000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45645-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431596","9783540456452"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-45645-7_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}