{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:29Z","timestamp":1781238929231,"version":"3.54.1"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["197065"],"award-info":[{"award-number":["197065"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3. The resulting IVL program is then verified using an existing back-end verifier. A soundness proof for such a\n                    <jats:italic toggle=\"yes\">translational verifier<\/jats:italic>\n                    needs to relate the input program and verification logic to the semantics of the IVL, which in turn needs to be connected with the verification logic implemented in the back-end verifiers. Performing such proofs is challenging due to the large semantic gap between the input and output programs and logics, especially for complex verification logics such as separation logic.\n                  <\/jats:p>\n                  <jats:p>This paper presents a formal framework for reasoning about translational separation logic verifiers. At its center is a generic core IVL that captures the essence of different separation logics. We define its operational semantics and formally connect it to two different back-end verifiers, which use symbolic execution and verification condition generation, resp. Crucially, this semantics uses angelic non-determinism to enable the application of different proof search algorithms and heuristics in the back-end verifiers. An axiomatic semantics for the core IVL simplifies reasoning about the front-end translation by performing essential proof steps once and for all in the equivalence proof with the operational semantics rather than for each concrete front-end translation.<\/jats:p>\n                  <jats:p>We illustrate the usefulness of our formal framework by instantiating our core IVL with elements of Viper and connecting it to two Viper back-ends as well as a front-end for concurrent separation logic. All our technical results have been formalized in Isabelle\/HOL, including the core IVL and its semantics, the semantics of two back-ends for a subset of Viper, and all proofs.<\/jats:p>","DOI":"10.1145\/3704856","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"569-599","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Formal Foundations for Translational Separation Logic Verifiers"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2719-4856","authenticated-orcid":false,"given":"Thibault","family":"Dardinier","sequence":"first","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1816-9256","authenticated-orcid":false,"given":"Gaurav","family":"Parthasarathy","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-9381","authenticated-orcid":false,"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_3_1","article-title":"A hybrid approach to semi-automated Rust verification","author":"Ayoun Sacha-\u00c9lie","year":"2024","unstructured":"Sacha-\u00c9lie Ayoun, Xavier Denis, Petar Maksimovic, and Philippa Gardner. 2024. A hybrid approach to semi-automated Rust verification. CoRR abs\/2403.15122 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2403.15122 10.48550\/ARXIV.2403.15122 arXiv:2403.15122","journal-title":"CoRR"},{"key":"e_1_3_2_4_1","doi-asserted-by":"crossref","unstructured":"Michael Backes Catalin Hritcu and Thorsten Tarrach. 2011. Automatically Verifying Typing Constraints for a Data Processing Language. In Certified Programs and Proofs (CPP) Jean-Pierre Jouannaud and Zhong Shao (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_22 10.1007\/978-3-642-25379-9_22","DOI":"10.1007\/978-3-642-25379-9_22"},{"key":"e_1_3_2_5_1","doi-asserted-by":"crossref","unstructured":"Josh Berdine Cristiano Calcagno and Peter W. O\u2019Hearn. 2005a. Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In FMCO (Lecture Notes in Computer Science Vol. 4111). Springer 115\u2013137. https:\/\/doi.org\/10.1007\/11804192_6 10.1007\/11804192_6","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_7_1","doi-asserted-by":"crossref","unstructured":"Stefan Blom Saeed Darabi Marieke Huisman and Wytse Oortwijn. 2017. The VerCors Tool Set: Verification of Parallel and Concurrent Software. In Integrated Formal Methods (IFM) Nadia Polikarpova and Steve Schneider (Eds.). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7 10.1007\/978-3-319-66845-1_7","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"e_1_3_2_8_1","doi-asserted-by":"crossref","unstructured":"Rastislav Bod\u00edk Satish Chandra Joel Galenson Doug Kimelman Nicholas Tung Shaon Barman and Casey Rodarmor. 2010. Programming with angelic nondeterminism. In POPL. ACM 339\u2013352. https:\/\/doi.org\/10.1145\/1706299.1706339 10.1145\/1706299.1706339","DOI":"10.1145\/1706299.1706339"},{"key":"e_1_3_2_9_1","doi-asserted-by":"crossref","unstructured":"John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis (SAS) Radhia Cousot (Ed.). 55\u201372. https:\/\/doi.org\/10.1007\/3-540-44898-5_4 10.1007\/3-540-44898-5_4","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_2_10_1","doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno Peter W. O\u2019Hearn and Hongseok Yang. 2007. Local Action and Abstract Separation Logic. In Logic in Computer Science (LICS). 366\u2013375. https:\/\/doi.org\/10.1109\/LICS.2007.30 10.1109\/LICS.2007.30","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_11_1","doi-asserted-by":"crossref","unstructured":"Qinxiang Cao Lennart Beringer Samuel Gruetter Josiah Dodds and Andrew W. Appel. 2018. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. J. Autom. Reason. 61 1-4 (2018) 367\u2013422. https:\/\/doi.org\/10.1007\/S10817-018-9457-5 10.1007\/S10817-018-9457-5","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632902"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563326"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586054"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_7"},{"key":"e_1_3_2_18_1","article-title":"Formal Foundations for Translational Separation Logic Verifiers (extended version)","author":"Dardinier Thibault","year":"2024","unstructured":"Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter M\u00fcller. 2024a. Formal Foundations for Translational Separation Logic Verifiers (extended version). CoRR abs\/2407.20002 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2407.20002 10.48550\/ARXIV.2407.20002","journal-title":"CoRR"},{"key":"e_1_3_2_19_1","unstructured":"Thibault Dardinier Michael Sammler Gaurav Parthasarathy Alexander J. Summers and Peter M\u00fcller. 2024b. Formal Foundations for Translational Separation Logic Verifiers \u2013 Artifact. https:\/\/doi.org\/10.5281\/zenodo.13938950 10.5281\/zenodo.13938950"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00527-y"},{"key":"e_1_3_2_21_1","doi-asserted-by":"crossref","unstructured":"Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In International Conference on Formal Engineering Methods (ICFEM) Adri\u00e1n Riesco and Min Zhang (Eds.) Vol. 13478. 90\u2013105. https:\/\/doi.org\/10.1007\/978-3-031-17244-1_6 10.1007\/978-3-031-17244-1_6","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_22_1","doi-asserted-by":"crossref","unstructured":"Robert Dockins Aquinas Hobor and Andrew W. Appel. 2009. A Fresh Look at Separation Algebras and Share Accounting. In Asian Symposium on Programming Languages and Systems (APLAS) Zhenjiang Hu (Ed.). 161\u2013177. https:\/\/doi.org\/10.1007\/978-3-642-10672-9_13 10.1007\/978-3-642-10672-9_13","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_3_2_23_1","unstructured":"Marco Eilers Malte Schwerhoff and Peter M\u00fcller. 2024. Verification Algorithms for Automated Separation Logic Verifiers. CoRR abs\/2405.10661 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2405.10661 10.48550\/ARXIV.2405.10661"},{"key":"e_1_3_2_24_1","doi-asserted-by":"crossref","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3 \u2014 Where Programs Meet Provers. In European Symposium on Programming (ESOP) Matthias Felleisen and Philippa Gardner (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8 10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_25_1","doi-asserted-by":"crossref","unstructured":"Robert W. Floyd. 1967. Nondeterministic Algorithms. J. ACM 14 4 (1967) 636\u2013644. https:\/\/doi.org\/10.1145\/321420.321422 10.1145\/321420.321422","DOI":"10.1145\/321420.321422"},{"key":"e_1_3_2_26_1","volume-title":"BSP-Why, un outil pour la v\u00e9rification d\u00e9ductive de programmes BSP: machine-checked semantics and application to distributed state-space algorithms. (BSP-Why, a tool for deductive verification of BSP programs: s\u00e9mantiques m\u00e9canis\u00e9es et application aux algorithmes d\u2019espace d\u2019\u00e9tats distribu\u00e9s)","author":"Fortin Jean","year":"2013","unstructured":"Jean Fortin. 2013. BSP-Why, un outil pour la v\u00e9rification d\u00e9ductive de programmes BSP: machine-checked semantics and application to distributed state-space algorithms. (BSP-Why, a tool for deductive verification of BSP programs: s\u00e9mantiques m\u00e9canis\u00e9es et application aux algorithmes d\u2019espace d\u2019\u00e9tats distribu\u00e9s). Ph. D. Dissertation. University of Paris-Est, France. https:\/\/tel.archives-ouvertes.fr\/tel-00974977"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473590"},{"key":"e_1_3_2_28_1","doi-asserted-by":"crossref","unstructured":"Quentin Garchery. 2021. A Framework for Proof-carrying Logical Transformations. In Workshop on Proof eXchange for Theorem Proving (PxTP) Chantal Keller and Mathias Fleury (Eds.). https:\/\/doi.org\/10.4204\/EPTCS.336.2 10.4204\/EPTCS.336.2","DOI":"10.4204\/EPTCS.336.0"},{"key":"e_1_3_2_29_1","doi-asserted-by":"crossref","unstructured":"Arma\u00ebl Gu\u00e9neau Johannes Hostert Simon Spies Michael Sammler Lars Birkedal and Derek Dreyer. 2023. Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proc. ACM Program. Lang. 7 OOPSLA2 (2023) 716\u2013744.","DOI":"10.1145\/3622823"},{"key":"e_1_3_2_30_1","volume-title":"Certification of a Tool Chain for Deductive Program Verification. (Certification d\u2019une chaine de v\u00e9rification d\u00e9ductive de programmes)","author":"Herms Paolo","year":"2013","unstructured":"Paolo Herms. 2013. Certification of a Tool Chain for Deductive Program Verification. (Certification d\u2019une chaine de v\u00e9rification d\u00e9ductive de programmes). Ph. D. Dissertation. University of Paris-Sud, Orsay, France. https:\/\/tel.archives-ouvertes.fr\/tel-00789543"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547628"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_3_2_35_1","first-page":"143","volume-title":"Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021","author":"Kragl Bernhard","year":"2021","unstructured":"Bernhard Kragl and Shaz Qadeer. 2021. The Civl Verifier. In Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021. IEEE, 143\u2013152. https:\/\/doi.org\/10.34727\/2021\/ISBN.978-3-85448-046-4_23 10.34727\/2021\/ISBN.978-3-85448-046-4_23"},{"key":"e_1_3_2_36_1","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. (2008). Available from http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml178.pdf."},{"key":"e_1_3_2_37_1","doi-asserted-by":"crossref","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming Artificial Intelligence and Reasoning (LPAR) Edmund M. Clarke and Andrei Voronkov (Eds.). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_38_1","doi-asserted-by":"crossref","unstructured":"K. Rustan M. Leino and Peter M\u00fcller. 2009. A Basis for Verifying Multi-threaded Programs. In European Symposium on Programming (ESOP) Giuseppe Castagna (Ed.) Vol. 5502. Springer 378\u2013393. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_27 10.1007\/978-3-642-00590-9_27","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_3_2_39_1","first-page":"25:1","volume-title":"ECOOP (LIPIcs","author":"L\u00f6\u00f6w Andreas","year":"2024","unstructured":"Andreas L\u00f6\u00f6w, Daniele Nantes-Sobrinho, Sacha-\u00c9lie Ayoun, Caroline Cronj\u00e4ger, Petar Maksimovic, and Philippa Gardner. 2024. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In ECOOP (LIPIcs, Vol. 313). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 25:1\u201325:28. https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2024.25 10.4230\/LIPICS.ECOOP.2024.25"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"e_1_3_2_41_1","unstructured":"Petar Maksimovic Jos\u00e9 Fragoso Santos Sacha-\u00c9lie Ayoun and Philippa Gardner. 2021b. Gillian: A Multi-Language Platform for Unified Symbolic Analysis. CoRR abs\/2105.14769 (2021). arXiv:2105.14769 https:\/\/arxiv.org\/abs\/2105.14769"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_22"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_45_1","first-page":"49","volume-title":"CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings (Lecture Notes in Computer Science","author":"O\u2019Hearn Peter W.","year":"2004","unstructured":"Peter W. O\u2019Hearn. 2004. Resources, Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings (Lecture Notes in Computer Science, Vol. 3170), Philippa Gardner and Nobuko Yoshida (Eds.). Springer, 49\u201367. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_4 10.1007\/978-3-540-28644-8_4"},{"issue":"3","key":"e_1_3_2_46_1","first-page":"1","article-title":"The Relationship Between Separation Logic and Implicit Dynamic Frames","volume":"8","author":"Parkinson Matthew J.","year":"2012","unstructured":"Matthew J. Parkinson and Alexander J. Summers. 2012. The Relationship Between Separation Logic and Implicit Dynamic Frames. Logical Methods in Computer Science 8, 3:01 (2012), 1\u201354. https:\/\/doi.org\/10.2168\/LMCS-8(3:1)2012 10.2168\/LMCS-8(3:1)2012","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656438"},{"key":"e_1_3_2_48_1","doi-asserted-by":"crossref","unstructured":"Gaurav Parthasarathy Peter M\u00fcller and Alexander J. Summers. 2021. Formally Validating a Practical Verification Condition Generator. In Computer Aided Verification (CAV) (LNCS Vol. 12760) Alexandra Silva and K. Rustan M. Leino (Eds.). 704\u2013727. https:\/\/doi.org\/10.1007\/978-3-030-81688-9_33 10.1007\/978-3-030-81688-9_33","DOI":"10.1007\/978-3-030-81688-9_33"},{"key":"e_1_3_2_49_1","doi-asserted-by":"crossref","unstructured":"Ingrid Rewitzky. 2003. Binary Multirelations. In Theory and Applications of Relational Structures as Knowledge Instruments. LNCS Vol. 2929. Springer 256\u2013271. https:\/\/doi.org\/10.1007\/978-3-540-24615-2_12 10.1007\/978-3-540-24615-2_12","DOI":"10.1007\/978-3-540-24615-2_12"},{"key":"e_1_3_2_50_1","first-page":"55","article-title":"Separation logic: A logic for shared mutable data structures","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. Logic in Computer Science (LICS), 55\u201374. https:\/\/doi.org\/10.1109\/lics.2002.1029817 10.1109\/lics.2002.1029817","journal-title":"Logic in Computer Science (LICS)"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571220"},{"key":"e_1_3_2_53_1","first-page":"927","volume-title":"PLDI","author":"Santos Jos\u00e9 Fragoso","year":"2020","unstructured":"Jos\u00e9 Fragoso Santos, Petar Maksimovic, Sacha-\u00c9lie Ayoun, and Philippa Gardner. 2020. Gillian, Part i: A Multi-language Platform for Symbolic Execution. In PLDI. ACM, 927\u2013942. https:\/\/doi.org\/10.1145\/3385412.3386014 10.1145\/3385412.3386014"},{"key":"e_1_3_2_54_1","volume-title":"Advancing Automated, Permission-Based Program Verification Using Symbolic Execution","author":"Schwerhoff Malte","year":"2016","unstructured":"Malte Schwerhoff. 2016. Advancing Automated, Permission-Based Program Verification Using Symbolic Execution. Ph. D. Dissertation. ETH Zurich, Z\u00fcrich, Switzerland. https:\/\/doi.org\/10.3929\/ETHZ-A-010835519 10.3929\/ETHZ-A-010835519"},{"issue":"1","key":"e_1_3_2_55_1","first-page":"10:1","article-title":"Lightweight Support for Magic Wands in an Automatic Verifier (Artifact)","volume":"1","author":"Schwerhoff Malte","year":"2015","unstructured":"Malte Schwerhoff and Alexander J. Summers. 2015. Lightweight Support for Magic Wands in an Automatic Verifier (Artifact). Dagstuhl Artifacts Ser. 1, 1 (2015), 10:1\u201310:2. https:\/\/doi.org\/10.4230\/DARTS.1.1.10 10.4230\/DARTS.1.1.10","journal-title":"Dagstuhl Artifacts Ser"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00559-y"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_3_2_62_1","doi-asserted-by":"crossref","unstructured":"Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed separation logic: a program logic for C11 concurrency. In Object Oriented Programming Systems Languages & Applications (OOPSLA) Antony L. Hosking Patrick Th. Eugster and Cristina V. Lopes (Eds.). https:\/\/doi.org\/10.1145\/2509136.2509532 10.1145\/2509136.2509532","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_3_2_63_1","doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Vogels Bart Jacobs and Frank Piessens. 2009. A Machine Checked Soundness Proof for an Intermediate Verification Language. In Theory and Practice of Computer Science Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM) (Lecture Notes in Computer Science Vol. 5404) Mogens Nielsen Anton\u00edn Kucera Peter Bro Miltersen Catuscia Palamidessi Petr Tuma and Frank D. Valencia (Eds.). Springer 570\u2013581. https:\/\/doi.org\/10.1007\/978-3-540-95891-8_51 10.1007\/978-3-540-95891-8_51","DOI":"10.1007\/978-3-540-95891-8_51"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1774088.1774610"},{"issue":"3","key":"e_1_3_2_65_1","article-title":"Featherweight VeriFast","volume":"11","author":"Vogels Fr\u00e9d\u00e9ric","year":"2015","unstructured":"Fr\u00e9d\u00e9ric Vogels, Bart Jacobs, and Frank Piessens. 2015. Featherweight VeriFast. Log. Methods Comput. Sci. 11, 3 (2015). https:\/\/doi.org\/10.2168\/LMCS-11(3:19)2015 10.2168\/LMCS-11(3:19)2015","journal-title":"Log. Methods Comput. Sci"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-023-00427-w"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632927"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704856","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704856","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:34Z","timestamp":1770200194000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704856"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":66,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704856"],"URL":"https:\/\/doi.org\/10.1145\/3704856","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}