{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T15:17:53Z","timestamp":1770391073325,"version":"3.49.0"},"reference-count":75,"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\/501100001459","name":"Singapore's Ministry of Education","doi-asserted-by":"crossref","award":["MOE-T1-1\/2022-43"],"award-info":[{"award-number":["MOE-T1-1\/2022-43"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001475","name":"Nanyang Technological University","doi-asserted-by":"publisher","award":["Nanyang Assistant Professorship Start-Up Grant"],"award-info":[{"award-number":["Nanyang Assistant Professorship Start-Up Grant"]}],"id":[{"id":"10.13039\/501100001475","id-type":"DOI","asserted-by":"publisher"}]}],"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>Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs. The need for verifying complex programs compels it to involve expressive Separation Logics (SLs) that exceed the scopes of well-studied automated proof theories, e.g., symbolic heap. Consequently, automation of SL in foundational verification relies heavily on ad-hoc heuristics that lack a systematic meta-theory and face scalability issues. To mitigate the gap, we propose a theory to specify SL predicates using abstract algebras including functors, homomorphisms, and modules over rings. Based on this theory, we develop a generic SL automation algorithm to reason about any data structures that can be characterized by these algebras. In addition, we also present algorithms for automatically instantiating the algebraic models to real data structures. The instantiation works compositionally, reusing the algebraic models of component structures and preserving their data abstractions. Case studies on formalized imperative semantics show our algorithm can instantiate the algebraic models automatically for a variety of complex data structures. Experimental results indicate the automatically instantiated reasoners from our generic theory show similar results to the state-of-the-art systems made of specifically crafted reasoning rules. The presented theories, proofs, and the verification framework are formalized in Isabelle\/HOL.<\/jats:p>","DOI":"10.1145\/3704903","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1992-2024","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Generically Automating Separation Logic by Functors, Homomorphisms, and Modules"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9196-3237","authenticated-orcid":false,"given":"Qiyuan","family":"Xu","sequence":"first","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2755-3089","authenticated-orcid":false,"given":"David","family":"Sanan","sequence":"additional","affiliation":[{"name":"Singapore Institute of Technology, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7164-0580","authenticated-orcid":false,"given":"Zhe","family":"Hou","sequence":"additional","affiliation":[{"name":"Griffith University, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5878-6486","authenticated-orcid":false,"given":"Xiaokun","family":"Luan","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0596-877X","authenticated-orcid":false,"given":"Conrad","family":"Watt","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7300-9215","authenticated-orcid":false,"given":"Yang","family":"Liu","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_2_3_2","first-page":"97","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"Berdine Josh","year":"2005","unstructured":"Josh Berdine, Cristiano Calcagno, and Peter W. O\u2019Hearn. 2005. A Decidable Fragment of Separation Logic. In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, Kamal Lodaya and Meena Mahajan (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 97\u2013109."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0002-4"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_12"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_29"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837621"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Dino Distefano Peter O\u2019Hearn and Hongseok Yang. 2009. Compositional shape analysis by means of bi-abduction. SIGPLAN Not. 44 1 (jan 2009) 289\u2013300. https:\/\/doi.org\/10.1145\/1594834.1480917 10.1145\/1594834.1480917","DOI":"10.1145\/1594834.1480917"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Peter W. O\u2019Hearn and Hongseok Yang. 2007. Local Action and Abstract Separation Logic. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007). 366\u2013378. https:\/\/doi.org\/10.1109\/LICS.2007.30 10.1109\/LICS.2007.30","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","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. Journal of Automated Reasoning 61 1 (01 Jun 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_14_2","doi-asserted-by":"publisher","unstructured":"Adam Chlipala. 2011. Mostly-automated verification of low-level programs in computational separation logic. SIGPLAN Not. 46 6 (jun 2011) 234\u2013245. https:\/\/doi.org\/10.1145\/1993316.1993526 10.1145\/1993316.1993526","DOI":"10.1145\/1993316.1993526"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Adam Chlipala. 2013. The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. SIGPLAN Not. 48 9 (sep 2013) 391\u2013402. https:\/\/doi.org\/10.1145\/2544174.2500592 10.1145\/2544174.2500592","DOI":"10.1145\/2544174.2500592"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677003"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Hoang-Hai Dang Jacques-Henri Jourdan Jan-Oliver Kaiser and Derek Dreyer. 2019. RustBelt meets relaxed memory. Proc. ACM Program. Lang. 4 POPL Article 34 (dec 2019) 29 pages. https:\/\/doi.org\/10.1145\/3371102 10.1145\/3371102","DOI":"10.1145\/3371102"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Thibault Dardinier Peter M\u00fcller and Alexander J. Summers. 2022. Fractional resources in unbounded separation logic. Proc. ACM Program. Lang. 6 OOPSLA2 Article 163 (Oct. 2022) 27 pages. https:\/\/doi.org\/10.1145\/3563326 10.1145\/3563326","DOI":"10.1145\/3563326"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Thomas Dinsdale-Young Lars Birkedal Philippa Gardner Matthew Parkinson and Hongseok Yang. 2013. Views: compositional reasoning for concurrent programs. SIGPLAN Not. 48 1 (jan 2013) 287\u2013300. https:\/\/doi.org\/10.1145\/2480359.2429104 10.1145\/2480359.2429104","DOI":"10.1145\/2480359.2429104"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2021.20"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Constantin Enea Ondrej Leng\u00e1l Mihaela Sighireanu and Tom\u00e1\u0161 Vojnar. 2017. Compositional entailment checking for a fragment of separation logic. Formal Methods in System Design 51 3 (01 Dec 2017) 575\u2013607. https:\/\/doi.org\/10.1007\/s10703-017-0289-4 10.1007\/s10703-017-0289-4","DOI":"10.1007\/s10703-017-0289-4"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_3"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Lennard G\u00e4her Michael Sammler Ralf Jung Robbert Krebbers and Derek Dreyer. 2024. RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. 8 PLDI Article 192 (jun 2024) 25 pages. https:\/\/doi.org\/10.1145\/3656422 10.1145\/3656422","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594296"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Ronghui Gu Zhong Shao Hao Chen Jieung Kim J\u00e9r\u00e9mie Koenig Xiongnan (Newman) Wu Vilhelm Sj\u00f6berg and David Costanzo. 2019. Building certified concurrent OS kernels. Commun. ACM 62 10 (sep 2019) 89\u201399. https:\/\/doi.org\/10.1145\/3356903 10.1145\/3356903","DOI":"10.1145\/3356903"},{"key":"e_1_3_2_28_2","first-page":"653","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_34"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-8785-0"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Samin S. Ishtiaq and Peter W. O\u2019Hearn. 2001. BI as an assertion language for mutable data structures. SIGPLAN Not. 36 3 (jan 2001) 14\u201326. https:\/\/doi.org\/10.1145\/373243.375719 10.1145\/373243.375719","DOI":"10.1145\/373243.375719"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_23"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2017. RustBelt: securing the foundations of the Rust programming language. Proc. ACM Program. Lang. 2 POPL Article 66 (dec 2017) 34 pages. https:\/\/doi.org\/10.1145\/3158154 10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018) e20. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1539-9_11"},{"key":"e_1_3_2_42_2","volume-title":"Automating Recursive Definitions and Termination Proofs in Higher-Order Logic","author":"Krauss Alexander","year":"2009","unstructured":"Alexander Krauss. 2009. Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Ph. D. Dissertation. Technische Universit\u00e4t M\u00fcnchen. https:\/\/mediatum.ub.tum.de\/681651"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_26"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_3"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_26"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52 7 (jul 2009) 107\u2013115. https:\/\/doi.org\/10.1145\/1538788.1538814 10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_24"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","unstructured":"William Mansky and Ke Du. 2024. An Iris Instance for Verifying CompCert C Programs. Proc. ACM Program. Lang. 8 POPL Article 6 (jan 2024) 27 pages. https:\/\/doi.org\/10.1145\/3632848 10.1145\/3632848","DOI":"10.1145\/3632848"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Kayvan Memarian Victor B. F. Gomes Brooks Davis Stephen Kell Alexander Richardson Robert N. M. Watson and Peter Sewell. 2019. Exploring C semantics and pointer provenance. Proc. ACM Program. Lang. 3 POPL Article 67 (jan 2019) 32 pages. https:\/\/doi.org\/10.1145\/3290380 10.1145\/3290380","DOI":"10.1145\/3290380"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"Juan Antonio Navarro P\u00e9rez and Andrey Rybalchenko. 2011. Separation logic + superposition calculus = heap theorem prover. SIGPLAN Not. 46 6 (jun 2011) 556\u2013566. https:\/\/doi.org\/10.1145\/1993316.1993563 10.1145\/1993316.1993563","DOI":"10.1145\/1993316.1993563"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_7"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Peter O\u2019Hearn. 2019. Separation logic. Commun. ACM 62 2 (jan 2019) 86\u201395. https:\/\/doi.org\/10.1145\/3211968 10.1145\/3211968","DOI":"10.1145\/3211968"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_12"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","unstructured":"Nadia Polikarpova and Ilya Sergey. 2019. Structuring the synthesis of heap-manipulating programs. Proc. ACM Program. Lang. 3 POPL Article 72 (jan 2019) 30 pages. https:\/\/doi.org\/10.1145\/3290385 10.1145\/3290385","DOI":"10.1145\/3290385"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"Jonathan Protzenko Jean-Karim Zinzindohou\u00e9 Aseem Rastogi Tahina Ramananandro Peng Wang Santiago Zanella-B\u00e9guelin Antoine Delignat-Lavaud C\u0103t\u0103lin Hri\u0163cu Karthikeyan Bhargavan C\u00e9dric Fournet and Nikhil Swamy. 2017. Verified low-level programming embedded in F*. Proc. ACM Program. Lang. 1 ICFP Article 17 (aug 2017) 29 pages. https:\/\/doi.org\/10.1145\/3110261 10.1145\/3110261","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","unstructured":"Christopher Pulte Dhruv C. Makwana Thomas Sewell Kayvan Memarian Peter Sewell and Neel Krishnaswami. 2023. CN: Verifying Systems C Code with Separation-Logic Refinement Types. 7 POPL Article 1 (jan 2023) 32 pages. https:\/\/doi.org\/10.1145\/3571194 10.1145\/3571194","DOI":"10.1145\/3571194"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_3_2_62_2","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"Roever Willem-Paul de","year":"2008","unstructured":"Willem-Paul de Roever and Kai Engelhardt. 2008. Data Refinement: Model-Oriented Proof Methods and their Comparison (1st ed.). Cambridge University Press, USA."},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018623"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","unstructured":"Simon Spies Lennard G\u00e4her Michael Sammler and Derek Dreyer. 2024. Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. Proc. ACM Program. Lang. 8 PLDI Article 183 ( jun 2024) 25 pages. https:\/\/doi.org\/10.1145\/3656413 10.1145\/3656413","DOI":"10.1145\/3656413"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_40"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","unstructured":"Quang-Trung Ta Ton Chanh Le Siau-Cheng Khoo and Wei-Ngan Chin. 2017. Automated lemma synthesis in symbolic-heap separation logic. Proc. ACM Program. Lang. 2 POPL Article 9 (dec 2017) 29 pages. https:\/\/doi.org\/10.1145\/3158097 10.1145\/3158097","DOI":"10.1145\/3158097"},{"key":"e_1_3_2_70_2","unstructured":"The Verifast Team. 2021. Verification of Matrix Multiplication. https:\/\/github.com\/verifast\/verifast\/blob\/c84c07bdfe777ce11a5c006975e35276ddee8bc0\/examples\/verifythis2016\/matmul.java published in Verifast project."},{"key":"e_1_3_2_71_2","unstructured":"The Verifast Team. 2021. Verification of Quicksort. https:\/\/github.com\/verifast\/verifast\/blob\/52db325f08149d1d1c4bfa13e204a4d3c903ee26\/examples\/quicksort.c published in Verifast project."},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21461-5_21"},{"key":"e_1_3_2_73_2","unstructured":"Qiyuan Xu. 2024. Phi-System. https:\/\/github.com\/xqyww123\/phi-system"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","unstructured":"Qiyuan Xu. 2024. The Artifact of \u201cGenerically Automating Separation Logic by Functors Homomorphisms and Modules\u201d\u2019. https:\/\/doi.org\/10.5281\/zenodo.14207756 10.5281\/zenodo.14207756","DOI":"10.5281\/zenodo.14207756"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/3617232.3624859"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","unstructured":"Litao Zhou Jianxing Qin Qinshi Wang Andrew W. Appel and Qinxiang Cao. 2024. VST-A: A Foundationally Sound Annotation Verifier. Proc. ACM Program. Lang. 8 POPL Article 69 (jan 2024) 30 pages. https:\/\/doi.org\/10.1145\/3632911 10.1145\/3632911","DOI":"10.1145\/3632911"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704903","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704903","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:40Z","timestamp":1770200260000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704903"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":75,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704903"],"URL":"https:\/\/doi.org\/10.1145\/3704903","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"}}]}}