{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:32:26Z","timestamp":1768343546339,"version":"3.49.0"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030587673","type":"print"},{"value":"9783030587680","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-58768-0_11","type":"book-chapter","created":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:02:48Z","timestamp":1599825768000},"page":"193-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Hoare-Style Logic for Unstructured Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9921-3257","authenticated-orcid":false,"given":"Didrik","family":"Lundberg","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8069-6495","authenticated-orcid":false,"given":"Roberto","family":"Guanciale","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5311-1781","authenticated-orcid":false,"given":"Andreas","family":"Lindner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5432-6442","authenticated-orcid":false,"given":"Mads","family":"Dam","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,8]]},"reference":[{"key":"11_CR1","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 247\u2013256. IEEE (2001)"},{"issue":"2","key":"11_CR2","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF00264021","volume":"11","author":"MA Arbib","year":"1979","unstructured":"Arbib, M.A., Alagi\u0107, S.: Proof rules for gotos. Acta Informatica 11(2), 139\u2013148 (1979). \nhttps:\/\/doi.org\/10.1007\/BF00264021","journal-title":"Acta Informatica"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Ashcroft, E., Hoare, C.A.R., et al.: Remarks on \u201cprogram proving: jumps and functions\u201d by M. Clint and C.A.R. Hoare. Acta Informatica 6, 317\u2013318 (1976)","DOI":"10.1007\/BF00288660"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 82\u201387 (2005)","DOI":"10.1145\/1108792.1108813"},{"key":"11_CR5","unstructured":"Bartels, B.: A mechanized verification environment for real-time process algebras and low-level programming languages. Ph.D. thesis, Technical University of Berlin (2014)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Bartels, B., Glesner, S.: Verification of distributed embedded real-time systems and their low-level implementations using timed CSP. In: 2011 18th Asia-Pacific Software Engineering Conference, pp. 195\u2013202. IEEE (2011)","DOI":"10.1109\/APSEC.2011.52"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-06200-6_8","volume-title":"NASA Formal Methods","author":"B Bartels","year":"2014","unstructured":"Bartels, B., J\u00e4hnig, N.: Mechanized, compositional verification of low-level code. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 98\u2013112. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-06200-6_8"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Laporte, V.: Secure compilation of side-channel countermeasures: the case of cryptographic \u201cconstant-time\u201d. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 328\u2013343. IEEE (2018)","DOI":"10.1109\/CSF.2018.00031"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11679219_9","volume-title":"Formal Aspects in Security and Trust","author":"G Barthe","year":"2006","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 112\u2013126. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11679219_9"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11575467_24","volume-title":"Programming Languages and Systems","author":"N Benton","year":"2005","unstructured":"Benton, N.: A typed, compositional logic for a stack-based abstract machine. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 364\u2013380. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11575467_24"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11874683_12","volume-title":"Computer Science Logic","author":"N Benton","year":"2006","unstructured":"Benton, N.: Abstracting allocation. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 182\u2013196. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11874683_12"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Benton, N., Zarfaty, U.: Formalizing and verifying semantic type soundness for a simple compiler (preliminary report). Technical report, Technical Report MSR-TR-2007-31, Microsoft Research (2007)","DOI":"10.1145\/1273920.1273922"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Benton, N., Zarfaty, U.: Formalizing and verifying semantic type soundness of a simple compiler. In: Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 1\u201312 (2007)","DOI":"10.1145\/1273920.1273922"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: Proceedings of the 2006 ACM Symposium on Applied Computing, pp. 1835\u20131839 (2006)","DOI":"10.1145\/1141277.1141708"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 234\u2013245 (2011)","DOI":"10.1145\/1993316.1993526"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: The bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, pp. 391\u2013402 (2013)","DOI":"10.1145\/2544174.2500592"},{"issue":"1","key":"11_CR17","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/BF00571463","volume":"2","author":"M Clint","year":"1973","unstructured":"Clint, M.: Program proving: coroutines. Acta Informatica 2(1), 50\u201363 (1973). \nhttps:\/\/doi.org\/10.1007\/BF00571463","journal-title":"Acta Informatica"},{"issue":"3","key":"11_CR18","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/BF00288686","volume":"1","author":"M Clint","year":"1972","unstructured":"Clint, M., Hoare, C.A.R.: Program proving: jumps and functions. Acta Informatica 1(3), 214\u2013224 (1972)","journal-title":"Acta Informatica"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Dam, M., Guanciale, R., Nemati, H.: Machine code verification of a tiny Arm hypervisor. In: Proceedings of the 3rd International Workshop on Trustworthy Embedded Devices, pp. 3\u201312 (2013)","DOI":"10.1145\/2517300.2517302"},{"key":"11_CR20","unstructured":"Danial, A.: Count Lines of Code (CLOC) (2020). \nhttps:\/\/github.com\/AlDanial\/cloc\n\n. version 1.86"},{"issue":"4","key":"11_CR21","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/BF00264536","volume":"15","author":"A De Bruin","year":"1981","unstructured":"De Bruin, A.: Goto statements: semantics and deduction systems. Acta Informatica 15(4), 385\u2013424 (1981). \nhttps:\/\/doi.org\/10.1007\/BF00264536","journal-title":"Acta Informatica"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-10672-9_20","volume-title":"Programming Languages and Systems","author":"Y Dong","year":"2009","unstructured":"Dong, Y., Ren, K., Wang, S., Zhang, S.: Certify once, trust anywhere: modular certification of bytecode programs for certified virtual machine. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 275\u2013293. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-10672-9_20"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Dong, Y., Wang, S., Zhang, L., Yang, P.: Modular certification of low-level intermediate representation programs. In: 2009 33rd Annual IEEE International Computer Software and Applications Conference, vol. 1, pp. 563\u2013570. IEEE (2009)","DOI":"10.1109\/COMPSAC.2009.81"},{"key":"11_CR24","unstructured":"Duan, J.: Formal verification of device drivers in embedded systems. Ph.D. thesis, The University of Utah (2013)"},{"key":"11_CR25","unstructured":"Duan, J., Regehr, J.: Correctness proofs for device drivers in embedded systems. In: SSV (2010)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 67\u201378 (2007)","DOI":"10.1145\/1190315.1190325"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-87873-5_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"X Feng","year":"2008","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Combining domain-specific and foundational logics to verify complete software systems. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 54\u201369. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-87873-5_8"},{"issue":"6","key":"11_CR28","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1145\/1133255.1134028","volume":"41","author":"X Feng","year":"2006","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. ACM SIGPLAN Not. 41(6), 401\u2013414 (2006)","journal-title":"ACM SIGPLAN Not."},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-32347-8_23","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2012","unstructured":"Fox, A.: Directions in ISA specification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 338\u2013344. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32347-8_23"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-30569-9_8","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"R H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R., Mostowski, W.: Verification of safety properties in the presence of transactions. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 151\u2013171. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-30569-9_8"},{"issue":"10","key":"11_CR31","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"J\u00e4hnig, N., G\u00f6thel, T., Glesner, S.: A denotational semantics for communicating unstructured code. arXiv preprint \narXiv:1503.04913\n\n (2015)","DOI":"10.4204\/EPTCS.178.2"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-41591-8_5","volume-title":"Software Engineering and Formal Methods","author":"N J\u00e4hnig","year":"2016","unstructured":"J\u00e4hnig, N., G\u00f6thel, T., Glesner, S.: Refinement-based verification of communicating unstructured code. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 61\u201375. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41591-8_5"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"4","key":"11_CR35","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/BF00289468","volume":"7","author":"T Kowaltowski","year":"1977","unstructured":"Kowaltowski, T.: Axiomatic approach to side effects and general jumps. Acta Informatica 7(4), 357\u2013360 (1977). \nhttps:\/\/doi.org\/10.1007\/BF00289468","journal-title":"Acta Informatica"},{"issue":"1","key":"11_CR36","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/2578855.2535841","volume":"49","author":"R Kumar","year":"2014","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. ACM SIGPLAN Not. 49(1), 179\u2013191 (2014)","journal-title":"ACM SIGPLAN Not."},{"issue":"1","key":"11_CR37","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2007.02.059","volume":"190","author":"H Lehner","year":"2007","unstructured":"Lehner, H., M\u00fcller, P.: Formal translation of bytecode into BoogiePL. Electron. Not. Theor. Comput. Sci. 190(1), 35\u201350 (2007)","journal-title":"Electron. Not. Theor. Comput. Sci."},{"key":"11_CR38","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.scico.2019.01.001","volume":"174","author":"A Lindner","year":"2019","unstructured":"Lindner, A., Guanciale, R., Metere, R.: TrABin: trustworthy analyses of binaries. Sci. Comput. Program. 174, 72\u201389 (2019)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"11_CR39","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/BF00288637","volume":"3","author":"Z Manna","year":"1974","unstructured":"Manna, Z., Pnueli, A.: Axiomatic approach to total correctness of programs. Acta Informatica 3(3), 243\u2013263 (1974). \nhttps:\/\/doi.org\/10.1007\/BF00288637","journal-title":"Acta Informatica"},{"key":"11_CR40","unstructured":"Marti, N.: Formal verification of low-level software. Ph.D. thesis, University of Tokyo (2008)"},{"issue":"3","key":"11_CR41","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Trans. Program. Lang. Syst. (TOPLAS) 21(3), 527\u2013568 (1999)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"11_CR42","unstructured":"Myreen, M.O.: Formal verification of machine-code programs. Technical report. University of Cambridge, Computer Laboratory (2009)"},{"key":"11_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-03545-1_5","volume-title":"Certified Programs and Proofs","author":"MO Myreen","year":"2013","unstructured":"Myreen, M.O., Curello, G.: Proof pearl: a verified bignum implementation in x86-64 machine code. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 66\u201381. Springer, Cham (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-319-03545-1_5"},{"key":"11_CR44","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":"MO 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. 4424, pp. 568\u2013582. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71209-1_44"},{"key":"11_CR45","unstructured":"Myreen, M.O., Gordon, M.J.: Verification of machine code implementations of arithmetic functions for cryptography. In: Theorem Proving in Higher Order Logics: Emerging Trends Proceedings. Department of Computer Science, University of Kaiserslautern (2007)"},{"key":"11_CR46","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Gordon, M.J., Slind, K.: Machine-code verification for multiple architectures-an application of decompilation into logic. In: 2008 Formal Methods in Computer-Aided Design, pp. 1\u20138. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"11_CR47","unstructured":"Myreen, M.O., Gordon, M.J., Slind, K.: Decompilation into logic-improved. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 78\u201381. IEEE (2012)"},{"key":"11_CR48","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"11_CR49","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 320\u2013333 (2006)","DOI":"10.1145\/1111320.1111066"},{"issue":"12","key":"11_CR50","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1145\/358728.358748","volume":"25","author":"MJ O\u2019Donnell","year":"1982","unstructured":"O\u2019Donnell, M.J.: A critique of the foundations of Hoare style programming logics. Commun. ACM 25(12), 927\u2013935 (1982)","journal-title":"Commun. ACM"},{"key":"11_CR51","unstructured":"Saabas, A., Uustalu, T.: A compositional natural semantics and Hoare logic for low-level languages. Electron. Notes Theor. Comput. Sci. 156(1), 151\u2013168 (2006). \nhttp:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066106002222"},{"key":"11_CR52","doi-asserted-by":"crossref","unstructured":"Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471\u2013482 (2013)","DOI":"10.1145\/2499370.2462183"},{"key":"11_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","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. 3855, pp. 80\u201394. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11609773_6"},{"key":"11_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-319-29613-5_12","volume-title":"Verified Software: Theories, Tools, and Experiments","author":"J Tan","year":"2016","unstructured":"Tan, J., Tay, H.J., Gandhi, R., Narasimhan, P.: AUSPICE: automatic safety property verification for unmodified executables. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 202\u2013222. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-29613-5_12"},{"issue":"1","key":"11_CR55","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BF01940782","volume":"16","author":"A Wang","year":"1976","unstructured":"Wang, A.: An axiomatic basis for proving total correctness of goto-programs. BIT Numer. Math. 16(1), 88\u2013102 (1976). \nhttps:\/\/doi.org\/10.1007\/BF01940782","journal-title":"BIT Numer. Math."},{"key":"11_CR56","doi-asserted-by":"crossref","unstructured":"Wang, W., Shao, Z., Jiang, X., Guo, Y.: A simple model for certifying assembly programs with first-class function pointers. In: 2011 Fifth International Conference on Theoretical Aspects of Software Engineering, pp. 125\u2013132. IEEE (2011)","DOI":"10.1109\/TASE.2011.16"},{"key":"11_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36575-3_25","volume-title":"Programming Languages and Systems","author":"D Yu","year":"2003","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 363\u2013379. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/3-540-36575-3_25"},{"key":"11_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-030-02768-1_14","volume-title":"Programming Languages and Systems","author":"J Zha","year":"2018","unstructured":"Zha, J., Feng, X., Qiao, L.: Modular verification of SPARCv8 code. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 245\u2013263. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-02768-1_14"},{"key":"11_CR59","doi-asserted-by":"crossref","unstructured":"Zhao, L., Li, G., De Sutter, B., Regehr, J.: ARMor: fully verified software fault isolation. In: Proceedings of the Ninth ACM International Conference on Embedded Software, pp. 289\u2013298 (2011)","DOI":"10.1145\/2038642.2038687"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58768-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:04:01Z","timestamp":1599825841000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-58768-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030587673","9783030587680"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58768-0_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/event.cwi.nl\/sefm2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}