{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T01:12:27Z","timestamp":1773277947300,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540406648","type":"print"},{"value":"9783540451303","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_2","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T15:27:09Z","timestamp":1150730829000},"page":"25-40","source":"Crossref","is-referenced-by-count":44,"title":["Formal Specification and Verification of ARM6"],"prefix":"10.1007","author":[{"given":"Anthony","family":"Fox","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/3-540-44798-9_33","volume-title":"Correct Hardware Design and Verification Methods","author":"M.D. Aagaard","year":"2001","unstructured":"Aagaard, M.D., Cook, B., Day, N.A., Jones, R.B.: A framework for microprocessor correctness statements. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 433\u2013448. Springer, Heidelberg (2001)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-44659-1_2","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Barras","year":"2000","unstructured":"Barras, B.: Programming and computing in HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 17\u201337. Springer, Heidelberg (2000)"},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1023\/A:1014170513439","volume":"20","author":"S. Berezin","year":"2002","unstructured":"Berezin, S., Clarke, E., Biere, A., Zhu, Y.: Verification of out-of-order processor designs using model checking and a light-weight completion function. Formal Methods in System Design\u00a020(2), 187\u2013222 (2002)","journal-title":"Formal Methods in System Design"},{"key":"2_CR4","volume-title":"VLSI Specification, Verification and Synthesis","year":"1988","unstructured":"Birtwistle, G., Subrahmanyam, P.A. (eds.): VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, Dordrecht (1988)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0031816","volume-title":"Formal Methods in Computer-Aided Design","author":"B. Brock","year":"1996","unstructured":"Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 275\u2013293. Springer, Heidelberg (1996)"},{"issue":"2","key":"2_CR6","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF00243000","volume":"5","author":"A. Cohn","year":"1989","unstructured":"Cohn, A.: The notion of proof in hardware verification. Journal of Automated Reasoning\u00a05(2), 127\u2013139 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR7","unstructured":"Fox, A.C.J.: Algebraic Models for Advanced Microprocessors. PhD thesis, University of Wales Swansea (1998)"},{"key":"2_CR8","unstructured":"Fox, A.C.J.: An algebraic framework for modelling and verifying microprocessors using HOL. Technical Report 512, University of Cambridge, Computer Laboratory (April 2001)"},{"key":"2_CR9","unstructured":"Fox, A.C.J.: A HOL specification of the ARM instruction set architecture. Technical Report 545, University of Cambridge, Computer Laboratory (June 2001)"},{"key":"2_CR10","unstructured":"Fox, A.C.J.: Formal verification of the ARM6 micro-architecture. Technical Report 548, University of Cambridge, Computer Laboratory (November 2002)"},{"key":"2_CR11","series-title":"Kluwer International Series in Engineering and Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3576-8","volume-title":"The SECD Microprocessor, A Verification Case Study","author":"B.T. Graham","year":"1992","unstructured":"Graham, B.T.: The SECD Microprocessor, A Verification Case Study. Kluwer International Series in Engineering and Computer Science. Kluwer Academic Publishers, Dordrecht (1992)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/BFb0021717","volume-title":"Correct Hardware Design and Verification Methods","author":"N.A. Harman","year":"1993","unstructured":"Harman, N.A., Tucker, J.V.: Algebraic models and the correctness of microprocessors. In: Milne, G.J., Pierre, L. (eds.) CHARME 1993. LNCS, vol.\u00a0683, pp. 92\u2013108. Springer, Heidelberg (1993)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"FM8501: A Verified Microprocessor","author":"W.A. Hunt Jr.","year":"1994","unstructured":"Hunt Jr., W.A.: FM8501: A Verified Microprocessor. LNCS, vol.\u00a0795. Springer, Heidelberg (1994)"},{"key":"2_CR14","first-page":"35","volume-title":"Mechanized Reasoning and Hardware Design","author":"W.A. Hunt Jr.","year":"1992","unstructured":"Hunt Jr., W.A., Brock, B.C.: A formal HDL and its use in the FM9001 verification. In: Hoare, C.A.R., Gordon, M.J.C. (eds.) Mechanized Reasoning and Hardware Design, pp. 35\u201347. Prentice-Hall, Englewood Cliffs (1992)"},{"issue":"2","key":"2_CR15","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1023\/A:1014118529369","volume":"20","author":"R.B. Jones","year":"2002","unstructured":"Jones, R.B., Skakkeb\u00e6k, J.U., Dill, D.L.: Formal verification of out-of-order execution with incremental flushing. Formal Methods in System Design\u00a020(2), 139\u2013158 (2002)","journal-title":"Formal Methods in System Design"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Joyce, J.J.: Formal verification and implementation of a microprocessor. In: Birtwistle and Subrahmanyam [4], pp. 129\u2013157","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"2_CR17","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"1998","unstructured":"McMillan, K.: Verification of an implementation of tomasulo\u2019s algorithm by compositional model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Melham, T.F.: Abstraction mechanisms for hardware verification. In: Birtwistle and Subrahmanyam [4], pp. 267\u2013291","DOI":"10.1007\/978-1-4613-2007-4_9"},{"issue":"2","key":"2_CR20","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BF00122419","volume":"8","author":"S.P. Miller","year":"1996","unstructured":"Miller, S.P., Srivas, M.K.: Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Methods in Systems Design\u00a08(2), 153\u2013188 (1996)","journal-title":"Formal Methods in Systems Design"},{"issue":"2","key":"2_CR21","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1023\/A:1014122630277","volume":"20","author":"J. Sawada","year":"2002","unstructured":"Sawada, J., Hunt Jr., W.A.: Verification of FM9801: An out-of-order model with speculative execution, exceptions, and program-modifying capability. Formal Methods in System Design\u00a020(2), 187\u2013222 (2002)","journal-title":"Formal Methods in System Design"},{"key":"2_CR22","volume-title":"ARM Architectural Reference Manual","year":"2001","unstructured":"Seal, D. (ed.): ARM Architectural Reference Manual, 2nd edn. Addison-Wesley, Reading (2001)","edition":"2"},{"issue":"2","key":"2_CR23","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1023\/A:1008622002590","volume":"13","author":"S. Tahar","year":"2002","unstructured":"Tahar, S., Kumar, R.: A practical methodology for the formal verification of RISC processors. Formal Methods in System Design\u00a013(2), 159\u2013225 (2002)","journal-title":"Formal Methods in System Design"},{"issue":"34","key":"2_CR24","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1147\/rd.111.0025","volume":"11","author":"R.M. Tomasulo","year":"1967","unstructured":"Tomasulo, R.M.: An efficient algorithm for exploiting multiple arithmetic units. IBM Journal\u00a011(34), 25\u201333 (1967)","journal-title":"IBM Journal"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/3-540-59047-1_41","volume-title":"Theorem Provers in Circuit Design. Theory, Practice and Experience","author":"P.J. Windley","year":"1995","unstructured":"Windley, P.J., Coe, M.L.: A correctness model for pipelined microprocessors. In: Kumar, R., Kropf, T. (eds.) TPCD 1994. LNCS, vol.\u00a0901, pp. 33\u201351. Springer, Heidelberg (1995)"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/3-540-57826-9_149","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"W. Wong","year":"1994","unstructured":"Wong, W.: Modelling bit vectors in HOL: The word library. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol.\u00a0780, pp. 371\u2013384. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10930755_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T01:26:30Z","timestamp":1552613190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/10930755_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}