{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:56Z","timestamp":1740122696842,"version":"3.37.3"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1005849","1521602"],"award-info":[{"award-number":["1005849","1521602"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,10]]},"DOI":"10.1007\/s10703-020-00353-1","type":"journal-article","created":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T19:03:57Z","timestamp":1616526237000},"page":"322-345","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Abstraction and subsumption in modular verification of C programs"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1570-3492","authenticated-orcid":false,"given":"Lennart","family":"Beringer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"353_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive software verification-the key book, volume 10001 of lecture notes in computer science","author":"W Ahrendt","year":"2016","unstructured":"Ahrendt W, Beckert B, Bubel R, H\u00e4hnle R, Schmitt PH, Ulbrich M (2016) Deductive software verification-the key book, volume 10001 of lecture notes in computer science. Springer, New York"},{"issue":"3","key":"353_CR2","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0022-0000(89)90027-5","volume":"39","author":"P America","year":"1989","unstructured":"America P, Rutten J (1989) Solving reflexive domain equations in a category of complete metric spaces. J Comput Syst Sci 39(3):343\u2013375","journal-title":"J Comput Syst Sci"},{"issue":"2","key":"353_CR3","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/2701415","volume":"37","author":"AW Appel","year":"2015","unstructured":"Appel AW (2015) Verification of a cryptographic primitive: SHA-256. ACM Trans Program Lang Syst 37(2):7:1\u20137:31","journal-title":"ACM Trans Program Lang Syst"},{"key":"353_CR4","unstructured":"Appel AW, Beringer L, Cao Q, Dodds J (2019) Verifiable C: applying the verified software toolchain to C programs. https:\/\/vst.cs.princeton.edu\/download\/VC.pdf. Accessed 10 Sept 2020"},{"key":"353_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program logics for certified compilers","author":"AW Appel","year":"2014","unstructured":"Appel AW, Dockins R, Hobor A, Beringer L, Dodds J, Stewart G, Blazy S, Leroy X (2014) Program logics for certified compilers. Cambridge University Press, Cambridge"},{"key":"353_CR6","doi-asserted-by":"crossref","unstructured":"Appel AW, Naumann DA (2020) Verified sequential malloc\/free. In: Proceedings of the 2020 ACM SIGPLAN international symposium on memory management, pp 48\u201359","DOI":"10.1145\/3381898.3397211"},{"key":"353_CR7","doi-asserted-by":"crossref","unstructured":"Beringer Lennart (2011) Relational decomposition. In: Interactive theorem proving (LNCS 6898). Springer, Berlin, pp 39\u201354","DOI":"10.1007\/978-3-642-22863-6_6"},{"key":"353_CR8","series-title":"LNCS","first-page":"573","volume-title":"Formal methods\u2014the next 30 years\u2014third world congress, FM 2019, proceedings","author":"L Beringer","year":"2019","unstructured":"Beringer L, Appel AW (2019) Abstraction and subsumption in modular verification of C programs. In: ter Beek Maurice H, Annabelle M, Oliveira JN (eds) Formal methods\u2014the next 30 years\u2014third world congress, FM 2019, proceedings, vol 11800. LNCS. Springer, New York, pp 573\u2013590"},{"key":"353_CR9","unstructured":"Beringer L, Petcher A, Katherine\u00a0QY, Appel AW (2015) Verified correctness and security of OpenSSL HMAC. In: 24th USENIX Security Symposium. USENIX Assocation, pp 207\u2013221"},{"issue":"1\u20134","key":"353_CR10","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","volume":"61","author":"Q Cao","year":"2018","unstructured":"Cao Q, Beringer L, Gruetter S, Dodds J, Appel AW (2018) VST-Floyd: a separation logic tool to verify correctness of C programs. J Autom Reason 61(1\u20134):367\u2013422","journal-title":"J Autom Reason"},{"key":"353_CR11","doi-asserted-by":"crossref","unstructured":"Chajed T Tassarotti J, Kaashoek MF, Zeldovich N (2019) Verifying concurrent, crash-safe systems with perennial. In: Brecht T, Williamson C (eds) Proceedings of the 27th ACM symposium on operating systems principles, SOSP 2019, Huntsville, ON, Canada, October 27\u201330, 2019. ACM, pp 243\u2013258","DOI":"10.1145\/3341301.3359632"},{"key":"353_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"theorem proving in higher order logics, 22nd international conference, TPHOLs 2009, proceedings","author":"E Cohen","year":"2009","unstructured":"Cohen E, Dahlweid M, Hillebrand MA, Leinenbach D, Moskal M, Santen T, Schulte W, Tobies S (2009) VCC: a practical system for verifying concurrent C. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) theorem proving in higher order logics, 22nd international conference, TPHOLs 2009, proceedings, vol 5674. Lecture Notes in Computer Science. Springer, New York, pp 23\u201342"},{"key":"353_CR13","unstructured":"Gerlach J, Efremov D, Sikatzki T, Brodmann M, Burghardt J, Carben A, Clausecker R, Gu L, Hartig K, Lapawczyk T, Pohl HW, Soto J, V\u00f6llinger K (2010) ACSL by example: towards a formally verified standard library, version 21.1.0. https:\/\/github.com\/fraunhoferfokus\/acsl-by-example. Accessed 10 Sept 2020"},{"key":"353_CR14","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic","author":"D Harel","year":"2000","unstructured":"Harel D, Kozen D, Tiuryn J (2000) Dynamic logic. MIT Press, Cambridge"},{"key":"353_CR15","doi-asserted-by":"crossref","unstructured":"Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F (2011) Verifast: a powerful, sound, predictable, fast verifier for C and Java. In: NASA formal methods symposium. Springer, pp 41\u201355","DOI":"10.1007\/978-3-642-20398-5_4"},{"issue":"POPL","key":"353_CR16","doi-asserted-by":"publisher","first-page":"66:1","DOI":"10.1145\/3158154","volume":"2","author":"R Jung","year":"2018","unstructured":"Jung R, Jourdan J-H, Krebbers R, Dreyer D (2018) Rustbelt: securing the foundations of the rust programming language. Proc ACM Program Lang 2(POPL):66:1\u201366:34","journal-title":"Proc ACM Program Lang"},{"key":"353_CR17","doi-asserted-by":"crossref","unstructured":"Jung R, Krebbers R, Jourdan J-H, Bizjak A, Birkedal L, Dreyer D (2018) Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J Funct Program 28:E20. https:\/\/doi.org\/10.1017S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"353_CR18","doi-asserted-by":"crossref","unstructured":"Kassios IT (2006) Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra J, Nipkow T, Sekerinski E (eds) FM 2006: Formal methods, 14th international symposium on formal methods, Hamilton, Canada, August 21\u201327, 2006, Proceedings, volume 4085 of Lecture Notes in Computer Science. Springer, pp 268\u2013283","DOI":"10.1007\/11813040_19"},{"issue":"3","key":"353_CR19","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2015) Frama-C: a software analysis perspective. Formal Asp Comput 27(3):573\u2013609","journal-title":"Formal Asp Comput"},{"issue":"5","key":"353_CR20","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T Kleymann","year":"1999","unstructured":"Kleymann T (1999) Hoare logic and auxiliary variables. Formal Asp Comput 11(5):541\u2013566","journal-title":"Formal Asp Comput"},{"key":"353_CR21","doi-asserted-by":"crossref","unstructured":"Koh N., Li Y., Li Y., Xia L-y, Beringer L, Honor\u00e9 W, Mansky W, Pierce BC, Zdancewic S (2019) From C to interaction trees: specifying, verifying, and testing a networked server. In: Proceedings of the 8th ACM SIGPLAN international conference on certified programs and proofs. ACM, pp 234\u2013248","DOI":"10.1145\/3293880.3294106"},{"issue":"4","key":"353_CR22","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/2766446","volume":"37","author":"GT Leavens","year":"2015","unstructured":"Leavens GT, Naumann DA (2015) Behavioral subtyping, specification inheritance, and modular reasoning. ACM Trans Program Lang Syst 37(4):13:1\u201313:88","journal-title":"ACM Trans Program Lang Syst"},{"key":"353_CR23","doi-asserted-by":"crossref","unstructured":"Rustan K, Leino M (2010) Dafny: an automatic program verifier for functional correctness. In: Clarke EM, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning\u201416th international conference, LPAR-16, Dakar, Senegal, April 25\u2013May 1, 2010, Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science. Springer, pp 348\u2013370","DOI":"10.1007\/978-3-642-17511-4_20"},{"issue":"7","key":"353_CR24","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7):107\u2013115","journal-title":"Commun ACM"},{"issue":"6","key":"353_CR25","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov B, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6):1811\u20131841","journal-title":"ACM Trans Program Lang Syst"},{"key":"353_CR26","doi-asserted-by":"crossref","unstructured":"Mansky W, Appel AW, Nogin A (2017) A verified messaging system. In: Proceedings of the 2017 ACM international conference on object oriented programming systems languages & applications, OOPSLA \u201917. ACM","DOI":"10.1145\/3133911"},{"issue":"3","key":"353_CR27","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1145\/44501.45065","volume":"10","author":"JC Mitchell","year":"1988","unstructured":"Mitchell JC, Plotkin GD (1988) Abstract types have existential type. ACM Trans Program Lang Syst 10(3):470\u2013502","journal-title":"ACM Trans Program Lang Syst"},{"key":"353_CR28","unstructured":"Naumann DA (1999) Deriving sharp rules of adaptation for Hoare logics. Technical Report 9906, Department of Computer Science, Stevens Institute of Technology"},{"key":"#cr-split#-353_CR29.1","doi-asserted-by":"crossref","unstructured":"Nipkow T (2002) Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield JC","DOI":"10.1007\/3-540-45793-3_8"},{"key":"#cr-split#-353_CR29.2","unstructured":"(ed) Computer science logic, 16th international workshop, CSL 2002, 11th annual conference of the EACSL, proceedings, volume 2471 of Lecture Notes in Computer Science. Springer, pp 103-119"},{"key":"353_CR30","doi-asserted-by":"crossref","unstructured":"Parkinson MJ, Bierman GM (2005) Separation logic and abstraction. In: 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2005), pp 247\u2013258","DOI":"10.1145\/1047659.1040326"},{"key":"353_CR31","volume-title":"Types and programming languages","author":"BC Pierce","year":"2002","unstructured":"Pierce BC (2002) Types and programming languages. MIT Press, Cambridge"},{"issue":"3","key":"353_CR32","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1016\/j.tcs.2005.06.018","volume":"343","author":"C Pierik","year":"2005","unstructured":"Pierik C, de Boer FS (2005) A proof outline logic for object-oriented programming. Theor Comput Sci 343(3):413\u2013442","journal-title":"Theor Comput Sci"},{"key":"353_CR33","doi-asserted-by":"crossref","unstructured":"Schmitt PH, Ulbrich M, Wei\u00df B (2010) Dynamic frames in java dynamic logic. In: Beckert B, March\u00e9 C (eds) formal verification of object-oriented software\u2014international conference, FoVeOOS 2010, Paris, France, June 28\u201330, 2010, Revised Selected Papers, volume 6528 of Lecture Notes in Computer Science. Springer, pp 138\u2013152","DOI":"10.1007\/978-3-642-18070-5_10"},{"key":"353_CR34","doi-asserted-by":"crossref","unstructured":"Schmitt PH, Ulbrich M, Wei\u00df B (2010) Dynamic frames in java dynamic logic\u2014formalization and proofs. Technical Report 2010\u20132011, KIT\u2014Karlsruher Institut f\u00fcr Tchnologie","DOI":"10.1007\/978-3-642-18070-5_10"},{"issue":"OOPSLA","key":"353_CR35","first-page":"17:11","volume":"3","author":"S Wang","year":"2019","unstructured":"Wang S, Cao Q, Mohan A, Hobor A (2019) Certifying graph-manipulating C programs via localizations within data structures. PACMPL 3(OOPSLA):17:11\u201317:130","journal-title":"PACMPL"},{"issue":"POPL","key":"353_CR36","first-page":"51:1","volume":"4","author":"L Xia","year":"2020","unstructured":"Xia L, Zakowski Y, He P, Hur C-K, Malecha G, Pierce BC, Zdancewic S (2020) Interaction trees: representing recursive and impure programs in coq. PACMPL 4(POPL):51:1\u201351:32","journal-title":"PACMPL"},{"key":"353_CR37","doi-asserted-by":"crossref","unstructured":"Ye KQ, Green M, Sanguansin N, Beringer L, Petcher A, Appel AW (2017) Verified correctness and security of mbedTLS HMAC-DRBG. In: Proceedings of the 2017 ACM SIGSAC conference on computer and communications security (CCS\u201917). ACM","DOI":"10.1145\/3133956.3133974"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00353-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00353-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00353-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,26]],"date-time":"2022-08-26T15:51:52Z","timestamp":1661529112000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00353-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,23]]},"references-count":38,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["353"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00353-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,3,23]]},"assertion":[{"value":"2 March 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}