{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:47:42Z","timestamp":1743119262318,"version":"3.40.3"},"publisher-location":"Boston, MA","reference-count":31,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781441915382"},{"type":"electronic","value":"9781441915399"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-4419-1539-9_8","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T00:26:11Z","timestamp":1267489571000},"page":"221-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Specification and Verification of ARM Hardware and Software"],"prefix":"10.1007","author":[{"given":"Anthony C. J.","family":"Fox","sequence":"first","affiliation":[]},{"given":"Michael J. C.","family":"Gordon","sequence":"additional","affiliation":[]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,1,23]]},"reference":[{"key":"8_CR1_8","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/1481839.1481842","volume-title":"Proceedings of the 4th ACM SIGPLAN workshop on declarative aspects of multicore programming","author":"J Alglave","year":"2009","unstructured":"Alglave J, Fox A, Ishtiaq S, Myreen M, Sarkar S, Sewell P, Nardelli FZ (2009) The semantics of Power and ARM multiprocessor machine code. In: Basin D, Wolff B (eds) Proceedings of the 4th ACM SIGPLAN workshop on declarative aspects of multicore programming. Association for Computing Machinery, New York, NY, pp 13\u201324"},{"key":"8_CR2_8","unstructured":"ARM Ltd. (2009) Jazelle technology. http:\/\/www.arm.com\/products\/multimedia\/java\/jazelle.html (accessed in July 2009)"},{"key":"8_CR3_8","first-page":"68","volume-title":"Automatic verification of pipelined microprocessor control","author":"J Burch","year":"1994","unstructured":"Burch J, Dill D (1994) Automatic verification of pipelined microprocessor control. Springer, Berlin, pp 68\u201380"},{"key":"8_CR4_8","volume-title":"Algebraic models for advanced microprocessors","author":"ACJ Fox","year":"1998","unstructured":"Fox ACJ (1998) Algebraic models for advanced microprocessors. PhD thesis, University of Wales, Swansea"},{"key":"8_CR5_8","unstructured":"Fox ACJ (2001a) An algebraic framework for modelling and verifying microprocessors using HOL. In: Technical report 512, University of Cambridge Computer Laboratory, April 2001"},{"key":"8_CR6_8","unstructured":"Fox ACJ (2001b). A HOL specification of the ARM instruction set architecture. In: Technical report 545, University of Cambridge Computer Laboratory, June 2001"},{"key":"8_CR7_8","unstructured":"Fox ACJ (2002) Formal verification of the ARM6 micro-architecture. In: Technical report 548, University of Cambridge, Computer Laboratory, 2002"},{"key":"8_CR8_8","series-title":"of Lecture notes in computer science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10930755_2","volume-title":"Theorem proving in higher order logics","author":"ACJ Fox","year":"2003","unstructured":"Fox ACJ (2003) Formal specification and verification of ARM6. In: Basin D, Wolff B (eds) Theorem proving in higher order logics, vol 2758 of Lecture notes in computer science. Springer, Berlin, pp 25\u201340"},{"key":"8_CR9_8","series-title":"of Lecture notes in computer science","first-page":"157","volume-title":"CALCO 2005","author":"ACJ Fox","year":"2005","unstructured":"Fox ACJ (2005) An algebraic framework for verifying the correctness of hardware with input and output: a formalization in HOL. In: Fiadeiro J, Harman N, Roggenbach M, Rutten JJMM (eds) CALCO 2005, vol 3629 of Lecture notes in computer science. Springer, Berlin, pp 157\u2013174"},{"key":"8_CR10_8","volume-title":"ARM: system-on-chip architecture","author":"S Furber","year":"2000","unstructured":"Furber S (2000) ARM: system-on-chip architecture, 2nd edn. Addison-Wesley, Reading, MA","edition":"2"},{"key":"8_CR11_8","unstructured":"Gordon M (2007) Defining a LISP interpreter in a logic of total functions. In: The ACL2 theorem prover and its applications (ACL2)"},{"key":"8_CR12_8","unstructured":"Gordon MJC (1983) Proving a computer correct with the LCF-LSM hardware verification system. In: Technical report 42, University of Cambridge Computer Laboratory, 1983"},{"key":"8_CR13_8","unstructured":"Greve D, Wilding M, Vanfleet WM (2003) A separation kernel formal security policy. In: ACL2 workshop 2003, June 2003"},{"key":"8_CR14_8","unstructured":"Greve D, Richards R, Wilding M (2004) A summary of intrinsic partitioning verification. In: ACL2 Workshop 2004, November 2004"},{"key":"8_CR15_8","doi-asserted-by":"crossref","unstructured":"Hardin D (2008) Invited tutorial: considerations in the design and verification of microprocessors for safety-critical and security-critical applications. In: Proceedings of FMCAD 2008, November 2008","DOI":"10.1109\/FMCAD.2008.ECP.5"},{"key":"8_CR16_8","first-page":"135","volume-title":"Mathematics of dependable systems II","author":"NA Harman","year":"1997","unstructured":"Harman NA, Tucker JV (1997) Algebraic models of microprocessors: the verification of a simple computer. In: Stavridou V (ed) Mathematics of dependable systems II. Oxford University Press, Oxford, pp 135\u2013170"},{"key":"8_CR17_8","series-title":"of Lecture notes in computer science, Oxford","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem proving in higher order logics, 18th International conference, TPHOLs 2005","author":"JR Harrison","year":"2005","unstructured":"Harrison JR (2005) A HOL theory of Euclidean space. In: Hurd J, Melham T (eds) Theorem proving in higher order logics, 18th International conference, TPHOLs 2005, vol 3603 of Lecture notes in computer science, Oxford, UK. Springer, Berlin, pp 114\u2013129"},{"key":"8_CR18_8","volume-title":"Formalizing elliptic curve cryptography in higher order logic","author":"J Hurd","year":"2005","unstructured":"Hurd J (2005) Formalizing elliptic curve cryptography in higher order logic. Available from the author\u2019s Web site, October 2005"},{"key":"8_CR19_8","unstructured":"Hurd J, Gordon M, Fox A (2006) Formalized elliptic curve cryptography. In: High confidence software and systems: HCSS 2006, April 2006"},{"key":"8_CR20_8","volume-title":"LISP 1.5 programmer\u2019s manual","author":"J McCarthy","year":"1966","unstructured":"McCarthy J, Abrahams PW, Edwards DJ, Hart TP, Levin MI (1966) LISP 1.5 programmer\u2019s manual. MIT, Cambridge, MA"},{"issue":"4","key":"8_CR21_8","first-page":"461","volume":"5","author":"JS Moore","year":"1989","unstructured":"Moore JS (foreword) (1989) Special issue on systems verification. J Autom Reason 5(4): 461\u2013492","journal-title":"J Autom Reason"},{"key":"8_CR22_8","unstructured":"Myreen MO (2009a) Formal verification of machine-code programs. PhD thesis, University of Cambridge"},{"key":"8_CR23_8","doi-asserted-by":"crossref","unstructured":"Myreen MO (2009b) Verified implementation of LISP on ARM, x86 and PowerPC. In: Theorem proving in higher-order logics (TPHOLs). Springer, Berlin","DOI":"10.1007\/978-3-642-03359-9_25"},{"key":"8_CR24_8","volume-title":"Formal methods in computer aided design (FMCAD)","author":"MO Myreen","year":"2008","unstructured":"Myreen MO, Slind K, Gordon MJC (2008) Machine-code verification for multiple architectures \u2013 an application of decompilation into logic. In: Formal methods in computer aided design (FMCAD). IEEE, New York, NY"},{"key":"8_CR25_8","volume-title":"Compiler construction (CC)","author":"MO Myreen","year":"2009","unstructured":"Myreen MO, Slind K, Gordon MJC (2009) Extensible proof-producing compilation. In: Compiler construction (CC). Springer, Heidelberg"},{"key":"8_CR26_8","volume-title":"Proceedings of logic in computer science (LICS)","author":"J Reynolds","year":"2002","unstructured":"Reynolds J (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of logic in computer science (LICS). IEEE Computer Society, Washington, DC"},{"issue":"2","key":"8_CR27_8","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1023\/A:1014122630277","volume":"20","author":"J Sawada","year":"2002","unstructured":"Sawada J, Hunt WA Jr (2002) Verification of fm9801: an out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability. Formal Methods Syst Des 20(2):187\u2013222","journal-title":"Formal Methods Syst Des"},{"key":"8_CR28_8","unstructured":"Schostak D (2003) Methodology for the formal specification of RTL RISC processor designs (with particular reference to the ARM6). PhD thesis, University of Leeds"},{"key":"8_CR29_8","unstructured":"Slind K (2009) TFL: an environment for terminating functional programs. http:\/\/www.cl.cam.ac.uk\/~ks121\/tfl.html (accessed in July 2009)"},{"key":"8_CR30_8","unstructured":"Thery L (2007) Proving the group law for elliptic curves formally. In: Technical report RT-0330, INRIA, 2007"},{"key":"8_CR31_8","unstructured":"Wong W (1983) Formal verification of VIPER \u2019s ALU. In: Technical report 300, University of Cambridge Computer Laboratory, April 1983"}],"container-title":["Design and Verification of Microprocessor Systems for High-Assurance Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-1539-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,5]],"date-time":"2024-08-05T17:05:23Z","timestamp":1722877523000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-1539-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781441915382","9781441915399"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_8","relation":{},"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"23 January 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}