{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T17:28:33Z","timestamp":1771954113882,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_18","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"243-258","source":"Crossref","is-referenced-by-count":85,"title":["A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture"],"prefix":"10.1007","author":[{"given":"Anthony","family":"Fox","sequence":"first","affiliation":[]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-68103-8_2","volume-title":"Types for Proofs and Programs","author":"R. Atkey","year":"2008","unstructured":"Atkey, R.: CoqJVM: An executable specification of the Java virtual machine using dependent types. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 18\u201332. Springer, Heidelberg (2008)"},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/1080091.1080123","volume-title":"Proceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications","author":"S. Bishop","year":"2005","unstructured":"Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. In: Proceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications, pp. 265\u2013276. ACM, New York (2005)"},{"key":"18_CR3","series-title":"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":"A. Fox","year":"2003","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 25\u201340. Springer, Heidelberg (2003)"},{"key":"18_CR4","volume-title":"ARM: system-on-chip architecture","author":"S. Furber","year":"2000","unstructured":"Furber, S.: ARM: system-on-chip architecture, 2nd edn. Addison-Wesley, Reading (2000)","edition":"2"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1217975.1217978","volume-title":"The ACL2 theorem prover and its applications (ACL2 \u201906)","author":"D.S. Hardin","year":"2006","unstructured":"Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: The ACL2 theorem prover and its applications (ACL2 \u201906), pp. 11\u201320. ACM, New York (2006)"},{"key":"18_CR6","volume-title":"Computer Architecture: A Quantitative Approach","author":"J.L. Hennessy","year":"2002","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 3rd edn. Morgan Kaufmann, San Francisco (2002)","edition":"3"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-02658-4_28","volume-title":"Computer Aided Verification","author":"W.A. Hunt Jr.","year":"2009","unstructured":"Hunt Jr., W.A., Swords, S.: Centaur technology media unit verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 353\u2013367. Springer, Heidelberg (2009)"},{"key":"18_CR8","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Symposium on Operating Systems Principles (SOSP)","author":"G. Klein","year":"2009","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220. ACM, New York (2009)"},{"issue":"4","key":"18_CR9","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Transactions on Programming Languages and Systems\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"18_CR10","first-page":"42","volume-title":"Principles of Programming Languages (POPL)","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages (POPL), pp. 42\u201354. ACM Press, New York (2006)"},{"key":"18_CR11","unstructured":"ARM Limited. ARM architecture reference manual: ARMv7-A and ARMv7-R edition. Technical Report ARM DDI 0406B, ARM Limited (2008)"},{"key":"18_CR12","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/858570.858572","volume-title":"Interpreters, virtual machines and emulators (IVME\u201903)","author":"H. Liu","year":"2003","unstructured":"Liu, H., Strother Moore, J.: Executable JVM model for analytical reasoning: a study. In: Interpreters, virtual machines and emulators (IVME\u201903), pp. 15\u201323. ACM, New York (2003)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/978-3-642-03359-9_25","volume-title":"TPHOLs","author":"M.O. Myreen","year":"2009","unstructured":"Myreen, M.O., Gordon, M.J.C.: Verified LISP implementations on ARM, x86 and PowerPC. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 359\u2013374. Springer, Heidelberg (2009)"},{"key":"18_CR14","unstructured":"Rivest, R.: The MD5 message-digest algorithm, http:\/\/www.ietf.org\/rfc\/rfc1321.txt (accessed, January 2010)"},{"key":"18_CR15","volume-title":"Principles of Programming Languages (POPL)","author":"S. Sarkar","year":"2009","unstructured":"Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-CC multiprocessor machine code. In: Principles of Programming Languages (POPL), ACM, New York (2009)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"18_CR17","unstructured":"Slind, K.X.: TFL: An environment for terminating functional programs, http:\/\/www.cl.cam.ac.uk\/~ks121\/tfl.html (accessed, January 2010)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Comprehending monads. In: Mathematical Structures in Computer Science, pp. 61\u201378 (1992)","DOI":"10.1017\/S0960129500001560"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,31]],"date-time":"2021-10-31T08:35:01Z","timestamp":1635669301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}