{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:56:34Z","timestamp":1774025794126,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540712084","type":"print"},{"value":"9783540712091","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_44","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T18:56:34Z","timestamp":1183575394000},"page":"568-582","source":"Crossref","is-referenced-by-count":30,"title":["Hoare Logic for Realistically Modelled Machine\u00a0Code"],"prefix":"10.1007","author":[{"given":"Magnus O.","family":"Myreen","sequence":"first","affiliation":[]},{"given":"Michael J. C.","family":"Gordon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"44_CR1","volume-title":"Proc. 16th IEEE Symposium on Logic in Computer Science (LICS)","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Proc. 16th IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"44_CR2","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF00264021","volume":"11","author":"M.A. Arbib","year":"1979","unstructured":"Arbib, M.A., Alagic, S.: Proof rules for gotos. Acta Informatica\u00a011, 139\u2013148 (1979)","journal-title":"Acta Informatica"},{"key":"44_CR3","unstructured":"Bevier, W.R.: A verified operating system kernel. PhD thesis, University of Texas at Austin (1987)"},{"issue":"1","key":"44_CR4","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"R.S. Boyer","year":"1996","unstructured":"Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM\u00a043(1), 166\u2013192 (1996), \n                    \n                      doi.acm.org\/10.1145\/227595.227603","journal-title":"J. ACM"},{"key":"44_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1049\/sej.1988.0012","volume":"3","author":"D.L. Clutterbuck","year":"1988","unstructured":"Clutterbuck, D.L.: The verification of low-level code. Software Engineering Journal\u00a03, 97\u2013111 (1988)","journal-title":"Software Engineering Journal"},{"key":"44_CR6","unstructured":"The HOL4\u00a0System (Description), \n                    \n                      http:\/\/hol.sourceforge.net\/documentation.html"},{"key":"44_CR7","doi-asserted-by":"crossref","unstructured":"Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: Manolios, P., Wilding, M. (eds.) Sixth International Workshop on the ACL2 Theorem Prover and Its Applications (2006)","DOI":"10.1145\/1217975.1217978"},{"key":"44_CR8","unstructured":"Klein, G., Tuch, H., Norrish, M.: Types, bytes, and separation logic. To appear in: Hofmann, M., Felleisen, M. (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2007)"},{"key":"44_CR9","volume-title":"Proceedings of the ACM SIGMINI\/SIGPLAN interface meeting on Programming systems in the small processor environment","author":"W.D. Maurer","year":"1976","unstructured":"Maurer, W.D.: Proving the correctness of a flight-director program for an airborne minicomputer. In: Proceedings of the ACM SIGMINI\/SIGPLAN interface meeting on Programming systems in the small processor environment, ACM Press, New York (1976), \n                    \n                      doi.acm.org\/10.1145\/800236.807101"},{"key":"44_CR10","series-title":"Lecture Notes in Computer Science","first-page":"272","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"A.C.J. Fox","year":"2007","unstructured":"Fox, A.C.J., Gordon, M.J.C., Myreen, M.O.: Hoare Logic for ARM Machine Code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol.\u00a04767, pp. 272\u2013286. Springer, Heidelberg (2007)"},{"key":"44_CR11","volume-title":"Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM Press, New York (1997), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/263699.263712"},{"key":"44_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Science Logic","author":"H. Yang","year":"2001","unstructured":"Yang, H., O\u2019Hearn, P.W., Reynolds, J.C.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, Springer, Heidelberg (2001)"},{"key":"44_CR13","volume-title":"Proceedings of 17th IEEE Symposium on Logic in Computer Science (LICS)","author":"J. Reynolds","year":"2002","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Proceedings of 17th IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, Los Alamitos (2002), \n                    \n                      citeseer.ist.psu.edu\/reynolds02separation.html"},{"issue":"1","key":"44_CR14","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/j.entcs.2005.09.031","volume":"156","author":"A. Saabas","year":"2006","unstructured":"Saabas, A., Uustalu, T.: A compositional natural semantics and hoare logic for low-level languages. Electronic Notes in Theoretical Computer Science\u00a0156(1), 151\u2013168 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"44_CR15","volume-title":"ARM Architecture Reference Manual","author":"D. Seal","year":"2000","unstructured":"Seal, D.: ARM Architecture Reference Manual. Addison-Wesley, Reading (2000)"},{"key":"44_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Tan","year":"2005","unstructured":"Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:16:52Z","timestamp":1605745012000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_44","relation":{},"subject":[]}}