{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:03Z","timestamp":1751660523022,"version":"3.40.3"},"publisher-location":"Cham","reference-count":68,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720186"},{"type":"electronic","value":"9783030720193"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modularity - the partitioning of software into units of functionality that interact with each other via interfaces - has been the mainstay of software development for half a century. In case of the C language, the main mechanism for modularity is the compilation unit \/ header file abstraction. This paper complements programmatic modularity for C with modularity idioms for specification and verification in the context of Verifiable C, an expressive separation logic for CompCert . Technical innovations include (i)<jats:italic>abstract predicate declarations<\/jats:italic>\u2013 existential packages that combine Parkinson &amp; Bierman\u2019s abstract predicates with their client-visible reasoning principles; (ii)<jats:italic>residual<\/jats:italic>predicates, which help enforcing data abstraction in callback-rich code; and (iii) an application to pure (Smalltalk-style) objects that connects code verification to model-level reasoning about features such as subtyping,<jats:italic>self<\/jats:italic>, inheritance, and late binding. We introduce our techniques using concrete example modules that have all been verified using the Coq proof assistant and combine to fully linked verified programs using a novel, abstraction-respecting component composition rule for Verifiable C.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_5","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"118-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verified Software Units"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1570-3492","authenticated-orcid":false,"given":"Lennart","family":"Beringer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Ahmed, A., Appel, A.W., Richards, C.D., Swadi, K.N., Tan, G., Wang, D.C.: Semantic foundations for typed assembly languages. ACM Trans. Program.Lang. Syst. 32(3), 7:1\u20137:67 (2010), https:\/\/doi.org\/10.1145\/1709093.1709094","DOI":"10.1145\/1709093.1709094"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Baader and Voronkov [7], pp. 380\u2013397, https:\/\/doi.org\/10.1007\/978-3-540-32275-7_25","DOI":"10.1007\/978-3-540-32275-7_25"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: LICS\u201901: 16th Annual IEEE Symposium on Logic in Computer Science, Proceedings. pp. 247\u2013256. IEEE Computer Society (2001), https:\/\/doi.org\/10.1109\/LICS.2001.932501","DOI":"10.1109\/LICS.2001.932501"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge (2014)","DOI":"10.1017\/CBO9781107256552"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Appel, A.W., Naumann, D.A.: Verified sequential malloc\/free. In: Ding, C., Maas, M. (eds.) ISMM\u201920: 2020 ACM SIGPLAN International Symposium on Memory Management. pp. 48\u201359. ACM (2020), https:\/\/doi.org\/10.1145\/3381898.3397211","DOI":"10.1145\/3381898.3397211"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J., Muntean, T. (eds.) CASSIS\u201904: International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Revised Selected Papers. LNCS, vol.\u00a03362, pp. 1\u201326. Springer (2004), https:\/\/doi.org\/10.1007\/978-3-540-30569-9_1","DOI":"10.1007\/978-3-540-30569-9_1"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Baader, F., Voronkov, A. (eds.): LPAR\u201904: Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, Proceedings, LNCS, vol.\u00a03452. Springer (2005), https:\/\/doi.org\/10.1007\/b106931","DOI":"10.1007\/b106931"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Balzer, R.M.: Dataless programming. In: American Federation of Information Processing Societies: Proceedings of the AFIPS \u201967 Fall Joint Computer Conference. AFIPS Conference Proceedings, vol.\u00a031, pp. 535\u2013544. AFIPS \/ ACM \/ Thomson Book Company, Washington D.C. (1967), https:\/\/doi.org\/10.1145\/1465611.1465683","DOI":"10.1145\/1465611.1465683"},{"key":"5_CR9","unstructured":"Balzer, S.: Rumer: A programming language and modular verification technique based on relationships. Ph.D. thesis, ETH Z\u00fcrich (2011)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Naumann, D.A.: Local reasoning for global invariants, part II: dynamic boundaries. J. ACM 60(3), 19:1\u201319:73 (2013), http:\/\/doi.acm.org\/10.1145\/2485981","DOI":"10.1145\/2487241.2485981"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27\u201356 (2004), https:\/\/doi.org\/10.5381\/jot.2004.3.6.a2","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D., Shankland, C. (eds.) Mathematics of Program Construction, 7th International Conference, MPC 2004, Proceedings. LNCS, vol.\u00a03125, pp. 54\u201384. Springer (2004), https:\/\/doi.org\/10.1007\/978-3-540-27764-4_5","DOI":"10.1007\/978-3-540-27764-4_5"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T.P., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: de\u00a0Boer, F.S., Bonsangue, M.M., Graf, S., de\u00a0Roever, W.P. (eds.) FMCO\u201907: Formal Methods for Components and Objects, 6th International Symposium, Revised Lectures. LNCS, vol.\u00a05382, pp. 1\u201324. Springer (2007), https:\/\/doi.org\/10.1007\/978-3-540-92188-2_1","DOI":"10.1007\/978-3-540-92188-2_1"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Beringer, L.: Verified Software Units \u2013 Coq development (2021), https:\/\/www.cs.princeton.edu\/~eberinge\/VSU_Esop21.tar.gz","DOI":"10.26226\/morressier.604907f41a80aac83ca25d1a"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Beringer, L., Appel, A.W.: Abstraction and subsumption in modular verification of C programs. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Proceedings. LNCS, vol. 11800, pp. 573\u2013590. Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-30942-8_34","DOI":"10.1007\/978-3-030-30942-8_34"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic certification of heap consumption. In: Baader and Voronkov [7], pp. 347\u2013362, https:\/\/doi.org\/10.1007\/978-3-540-32275-7_23","DOI":"10.1007\/978-3-540-32275-7_23"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Besson, F., Jensen, T.P., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364(3), 273\u2013291 (2006), https:\/\/doi.org\/10.1016\/j.tcs.2006.08.012","DOI":"10.1016\/j.tcs.2006.08.012"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Bruce, K.B., Cardelli, L., Pierce, B.C.: Comparing object encodings. Inf. Comput. 155(1-2), 108\u2013133 (1999),\u00a0https:\/\/doi.org\/10.1006\/inco.1999.2829","DOI":"10.1006\/inco.1999.2829"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: de\u00a0Boer, F.S., Bonsangue, M.M., Graf, S., de\u00a0Roever, W.P. (eds.) Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Revised Lectures. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer (2005), https:\/\/doi.org\/10.1007\/11804192_16","DOI":"10.1007\/11804192_16"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Clarke, D., Drossopoulou, S., Noble, J., Wrigstad, T.: Aliasing, confinement, and ownership in object-oriented programming. In: Cebulla, M. (ed.) Object-Oriented Technology. ECOOP 2007 Workshop Reader, Final Reports. LNCS, vol.\u00a04906, pp. 40\u201349. Springer (2007), https:\/\/doi.org\/10.1007\/978-3-540-78195-0_5","DOI":"10.1007\/978-3-540-78195-0_5"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Drossopoulou, S., Damiani, F., Dezani-Ciancaglini, M., Giannini, P.: Fickle : Dynamic object re-classification. In: Knudsen, J.L. (ed.) ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Proceedings. LNCS, vol.\u00a02072, pp. 130\u2013149. Springer (2001), https:\/\/doi.org\/10.1007\/3-540-45337-7_8","DOI":"10.1007\/3-540-45337-7_8"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Drossopoulou, S., Francalanza, A., M\u00fcller, P., Summers, A.J.: A unified framework for verification techniques for object invariants. In: Vitek, J. (ed.) ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Proceedings. LNCS, vol.\u00a05142, pp. 412\u2013437. Springer (2008), https:\/\/doi.org\/10.1007\/978-3-540-70592-5_18","DOI":"10.1007\/978-3-540-70592-5_18"},{"key":"5_CR23","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Longman Publishing Co., Inc, USA (1995)"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X.N., Weng, S., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. pp. 595\u2013608. ACM (2015), https:\/\/doi.org\/10.1145\/2676726.2676975","DOI":"10.1145\/2676726.2676975"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Gu, R., Shao, Z., Chen, H., Kim, J., Koenig, J., Wu, X.N., Sj\u00f6berg, V., Costanzo, D.: Building certified concurrent OS kernels. Commun. ACM 62(10), 89\u201399 (2019), https:\/\/doi.org\/10.1145\/3356903","DOI":"10.1145\/3356903"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Gu, R., Shao, Z., Kim, J., Wu, X.N., Koenig, J., Sj\u00f6berg, V., Chen, H., Costanzo, D., Ramananandro, T.: Certified concurrent abstraction layers. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018. pp. 646\u2013661. ACM (2018), https:\/\/doi.org\/10.1145\/3192366.3192381","DOI":"10.1145\/3192366.3192381"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. J. Autom. Reasoning 31(3-4), 191\u2013229 (2003), https:\/\/doi.org\/10.1023\/B:JARS.0000021012.97318.e9","DOI":"10.1023\/B:JARS.0000021012.97318.e9"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83\u201392 (2017), https:\/\/doi.org\/10.1145\/3068608","DOI":"10.1145\/3068608"},{"key":"5_CR29","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: End-to-end security via automated full-system verification. In: Flinn, J., Levy, H. (eds.) 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201914. pp. 165\u2013181. USENIX Association (2014), https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Hofmann, M., Pierce, B.C.: Positive subtyping. Inf. Comput. 126(1), 11\u201333 (1996), https:\/\/doi.org\/10.1006\/inco.1996.0031","DOI":"10.1006\/inco.1996.0031"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Honsell, F., Lenisa, M., Redamalla, R.: Coalgebraic semantics and observational equivalences of an imperative class-based OO-language. Electron. Notes Theor. Comput. Sci. 104, 163\u2013180 (2004), https:\/\/doi.org\/10.1016\/j.entcs.2004.08.024","DOI":"10.1016\/j.entcs.2004.08.024"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Huisman, M., Jacobs, B.: Inheritance in higher order logic: Modeling and reasoning. In: Theorem Proving in Higher Order Logics. LNCS, vol.\u00a01869, pp. 301\u2013319. Springer (2000)","DOI":"10.1007\/3-540-44659-1_19"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: Objects and classes, co-algebraically. In: Freitag, B., Jones, C.B., Lengauer, C., Schek, H. (eds.) Object Orientation with Parallelism and Persistence. pp. 83\u2013103. Kluwer Academic Publishers (1995)","DOI":"10.1007\/978-1-4613-1437-0_5"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: Verifast: A powerful, sound, predictable, fast verifier for C and java. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods - Third International Symposium, NFM 2011. Proceedings. LNCS, vol.\u00a06617, pp. 41\u201355. Springer (2011), https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"5_CR35","unstructured":"Jacobs, B., Smans, J., Piessens, F.: Verifying the composite pattern using separation logic. In: Specification and verification of component-based systems \u2013 Workshop at ACM SIGSOFT\/FSE 16 (2008), available at https:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"5_CR37","doi-asserted-by":"crossref","unstructured":"Kay, A.C.: The early history of Smalltalk. In: Lee, J.A.N., Sammet, J.E. (eds.) History of Programming Languages Conference (HOPL-II), Preprints. pp. 69\u201395. ACM (1993), https:\/\/doi.org\/10.1145\/154766.155364","DOI":"10.1145\/154766.155364"},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Formal Asp. Comput. 11(5), 541\u2013566 (1999), https:\/\/doi.org\/10.1007\/s001650050057","DOI":"10.1007\/s001650050057"},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Koh, N., Li, Y., Li, Y., Xia, L., Beringer, L., Honor\u00e9, W., Mansky, W., Pierce, B.C., Zdancewic, S.: From C to interaction trees: specifying, verifying, and testing a networked server. In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, (CPP\u201919). pp. 234\u2013248. ACM (2019), https:\/\/doi.org\/10.1145\/3293880.3294106","DOI":"10.1145\/3293880.3294106"},{"key":"5_CR40","unstructured":"Kravchuk-Kirilyuk, A.Y.: The B$$^{+}$$-tree Index as a Verified Software Unit. Master\u2019s thesis, Department of Computer Science, Princeton University (2020)"},{"key":"5_CR41","doi-asserted-by":"publisher","unstructured":"Krishnaswami, N.R., Aldrich, J., Birkedal, L., Svendsen, K., Buisse, A.: Design patterns in separation logic. In: Kennedy, A., Ahmed, A. (eds.) Proceedings of TLDI\u201909: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. pp. 105\u2013116. ACM (2009), https:\/\/doi.org\/10.1145\/1481861.1481874","DOI":"10.1145\/1481861.1481874"},{"key":"5_CR42","doi-asserted-by":"publisher","unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. ACM Trans. on Programming Languages and Systems 37(4), 13:1\u201313:88 (2015), https:\/\/doi.org\/10.1145\/2766446","DOI":"10.1145\/2766446"},{"key":"5_CR43","doi-asserted-by":"publisher","unstructured":"Liskov, B.: Keynote address - data abstraction and hierarchy. SIGPLAN Not. 23(5), 17\u201334 (Jan 1987), https:\/\/doi.org\/10.1145\/62139.62141","DOI":"10.1145\/62139.62141"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994), https:\/\/doi.org\/10.1145\/197320.197383","DOI":"10.1145\/197320.197383"},{"key":"5_CR45","doi-asserted-by":"publisher","unstructured":"McKinna, J., Burstall, R.M.: Deliverables: A categorial approach to program development in type theory. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS\u201993. Lecture Notes in Computer Science, vol.\u00a0711, pp. 32\u201367. Springer (1993), https:\/\/doi.org\/10.1007\/3-540-57182-5_3","DOI":"10.1007\/3-540-57182-5_3"},{"key":"5_CR46","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. on Programming Languages and Systems 10(3), 470\u2013502 (Jul 1988)","DOI":"10.1145\/44501.45065"},{"key":"5_CR47","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program. 62(3), 253\u2013286 (2006), https:\/\/doi.org\/10.1016\/j.scico.2006.03.001","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"5_CR48","unstructured":"Naumann, D.A.: Deriving sharp rules of adaptation for Hoare logics. Tech. Rep.\u00a09906, Department of Computer Science, Stevens Institute of Technology (1999)"},{"key":"5_CR49","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: Lee, P., Henglein, F., Jones, N.D. (eds.) Conference Record of POPL\u201997: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 106\u2013119. ACM Press (1997), https:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"5_CR50","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Proceedings. Lecture Notes in Computer Science, vol.\u00a02471, pp. 103\u2013119. Springer (2002), https:\/\/doi.org\/10.1007\/3-540-45793-3_8","DOI":"10.1007\/3-540-45793-3_8"},{"key":"5_CR51","doi-asserted-by":"publisher","unstructured":"Nistor, L., Aldrich, J., Balzer, S., Mehnert, H.: Object propositions. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. LNCS, vol.\u00a08442, pp. 497\u2013513. Springer (2014), https:\/\/doi.org\/10.1007\/978-3-319-06410-9_34","DOI":"10.1007\/978-3-319-06410-9_34"},{"key":"5_CR52","doi-asserted-by":"publisher","unstructured":"Nistor, L., Kurilova, D., Balzer, S., Chung, B., Potanin, A., Aldrich, J.: Wyvern: A simple, typed, and pure object-oriented language. In: Proceedings of the 5th Workshop on MechAnisms for SPEcialization, Generalization and InHerItance. pp. 9\u201316. MASPEGHI \u201913, Association for Computing Machinery, New York, NY, USA (2013), https:\/\/doi.org\/10.1145\/2489828.2489830","DOI":"10.1145\/2489828.2489830"},{"key":"5_CR53","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Separation logic. Commun. ACM 62(2), 86\u201395 (2019), https:\/\/doi.org\/10.1145\/3211968","DOI":"10.1145\/3211968"},{"key":"5_CR54","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. ACM Trans. Program. Lang. Syst. 31(3), 11:1\u201311:50 (2009), https:\/\/doi.org\/10.1145\/1498926.1498929.","DOI":"10.1145\/1498926.1498929"},{"key":"5_CR55","unstructured":"Parkinson, M.: Class invariants: the end of the road? (2007), contained in [20]. Also available at https:\/\/people.dsv.su.se\/~tobias\/iwaco\/p3-parkinson.pdf"},{"key":"5_CR56","doi-asserted-by":"publisher","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005. pp. 247\u2013258. ACM (2005), https:\/\/doi.org\/10.1145\/1040305.1040326","DOI":"10.1145\/1040305.1040326"},{"key":"5_CR57","doi-asserted-by":"publisher","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008. pp. 75\u201386. ACM (2008), https:\/\/doi.org\/10.1145\/1328438.1328451","DOI":"10.1145\/1328438.1328451"},{"key":"5_CR58","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge, Mass. (2002)"},{"key":"5_CR59","doi-asserted-by":"publisher","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A., Meyer, B.: Flexible invariants through semantic collaboration. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods - 19th International Symposium. LNCS, vol.\u00a08442, pp. 514\u2013530. Springer (2014), https:\/\/doi.org\/10.1007\/978-3-319-06410-9_35","DOI":"10.1007\/978-3-319-06410-9_35"},{"key":"5_CR60","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: GEDANKEN - a simple typeless language based on the principle of completeness and the reference concept. Commun. ACM 13(5), 308\u2013319 (1970), https:\/\/doi.org\/10.1145\/362349.362364","DOI":"10.1145\/362349.362364"},{"key":"5_CR61","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), Proceedings. pp. 55\u201374. IEEE Computer Society (2002), https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"5_CR62","doi-asserted-by":"publisher","unstructured":"Saini, D., Sunshine, J., Aldrich, J.: A theory of typestate-oriented programming. In: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010, Maribor, Slovenia, June 22, 2010. pp. 9:1\u20139:7. ACM (2010), https:\/\/doi.org\/10.1145\/1924520.1924529","DOI":"10.1145\/1924520.1924529"},{"key":"5_CR63","unstructured":"Schreiner, A.T.: Objektorientierte Programmierung mit ANSI-C. Hanser (1994), https:\/\/www.cs.rit.edu\/~ats"},{"key":"5_CR64","doi-asserted-by":"publisher","unstructured":"Sj\u00f6berg, V., Sang, Y., Weng, S.c., Shao, Z.: DeepSEA: A language for certified system software. Proc. ACM Program. Lang. 3(OOPSLA), 136:1\u2013136:27 (Oct 2019), https:\/\/doi.org\/10.1145\/3360562","DOI":"10.1145\/3360562"},{"key":"5_CR65","doi-asserted-by":"publisher","unstructured":"Summers, A.J., Drossopoulou, S.: Considerate reasoning and the composite design pattern. In: Barthe, G., Hermenegildo, M.V. (eds.) Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Proceedings. LNCS, vol.\u00a05944, pp. 328\u2013344. Springer (2010), https:\/\/doi.org\/10.1007\/978-3-642-11319-2_24","DOI":"10.1007\/978-3-642-11319-2_24"},{"key":"5_CR66","doi-asserted-by":"publisher","unstructured":"Summers, A.J., Drossopoulou, S., M\u00fcller, P.: The need for flexible object invariants. In: International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO\u201909). ACM (2009), https:\/\/doi.org\/10.1145\/1562154.1562160","DOI":"10.1145\/1562154.1562160"},{"key":"5_CR67","unstructured":"Vasudevan, A., Chaki, S., Maniatis, P., Jia, L., Datta, A.: \u00fcberspark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor. In: Holz, T., Savage, S. (eds.) 25th USENIX Security Symposium, USENIX Security 16. pp. 87\u2013104. USENIX Association (2016), https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/vasudevan"},{"key":"5_CR68","doi-asserted-by":"publisher","unstructured":"Xia, L., Zakowski, Y., He, P., Hur, C., Malecha, G., Pierce, B.C., Zdancewic, S.: Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4(POPL), 51:1\u201351:32 (2020), https:\/\/doi.org\/10.1145\/3371119","DOI":"10.1145\/3371119"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:46:46Z","timestamp":1671684406000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}