{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:46:38Z","timestamp":1777347998286,"version":"3.51.4"},"publisher-location":"Cham","reference-count":10,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319061993","type":"print"},{"value":"9783319062006","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06200-6_8","type":"book-chapter","created":{"date-parts":[[2014,4,23]],"date-time":"2014-04-23T01:53:48Z","timestamp":1398218028000},"page":"98-112","source":"Crossref","is-referenced-by-count":5,"title":["Mechanized, Compositional Verification of Low-Level Code"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Bartels","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nils","family":"J\u00e4hnig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","first-page":"1058","volume-title":"Certifying assembly with formal security proofs: The case of bbs","author":"R. Affeldt","year":"2012","unstructured":"Affeldt, R., Nowak, D., Yamada, K.: Certifying assembly with formal security proofs: The case of bbs, vol.\u00a077, pp. 1058\u20131074. Elsevier North-Holland, Inc., Amsterdam (2012)"},{"key":"8_CR2","unstructured":"Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical Report\u00a075, Dept. of Computer Science,University of Toronto (1975)"},{"key":"8_CR3","first-page":"301","volume-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013","author":"J.B. Jensen","year":"2013","unstructured":"Jensen, J.B., Benton, N., Kennedy, A.: High-level separation logic for low-level code. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 301\u2013314. ACM, New York (2013)"},{"key":"8_CR4","unstructured":"Jones, C.B.: Specification and Design of (Parallel) Programs. In: IFIP Congress, pp. 321\u2013332 (1983)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-540-71209-1_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.O. Myreen","year":"2007","unstructured":"Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 568\u2013582. Springer, Heidelberg (2007)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45793-3_8","volume-title":"Computer Science Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 103\u2013119. Springer, Heidelberg (2002)"},{"issue":"3","key":"8_CR8","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(83)90009-9","volume":"24","author":"E.-R. Olderog","year":"1983","unstructured":"Olderog, E.-R.: On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science\u00a024(3), 337\u2013347 (1983)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"8_CR9","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. Electron. Notes Theor. Comput. Sci.\u00a0156(1), 151\u2013168 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1007\/BFb0030635","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"T. Schreiber","year":"1997","unstructured":"Schreiber, T.: Auxiliary variables and recursive procedures. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 697\u2013711. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06200-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T13:29:15Z","timestamp":1558877355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06200-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319061993","9783319062006"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06200-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}