{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:06Z","timestamp":1775873406088,"version":"3.50.1"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"name":"Hakubi Center for Advanced Research","award":["Grant for Yusuke Matsushita"],"award-info":[{"award-number":["Grant for Yusuke Matsushita"]}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["KAKENHI Grant Numbers JP24KJ0133, JP22KJ0561, JP25H00446, JP23K24820, and JP20H05703"],"award-info":[{"award-number":["KAKENHI Grant Numbers JP24KJ0133, JP22KJ0561, JP25H00446, JP23K24820, and JP20H05703"]}],"id":[{"id":"10.13039\/501100001691","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,6,10]]},"abstract":"<jats:p>Separation logic (SL) has recently evolved at an exciting pace, opening the way to more complex goals, notably soundness proof of Rust's ownership type system and functional verification of Rust programs.  \nIn this paper, we address verification of termination in the presence of advanced features, especially Rust's ownership types.  \nPerhaps surprisingly, this goal cannot be achieved by a simple application of existing studies that dealt only with safety properties.  \nFor high-level reasoning about advanced shared mutable state as used in Rust, they used higher-order ghost state (i.e., logical state that depends on SL assertions), but in a way that depends on the later modality, a fundamental obstacle to verifying termination.<\/jats:p>\n          <jats:p>To solve this situation, we propose a novel general framework, Nola, which achieves later-free higher-order ghost state.  \nEven in the presence of advanced features such as invariants and borrows, Nola enables natural termination verification, allowing arbitrary induction in the meta-logic.  \nIts key idea is to parameterize higher-order ghost state, generalizing and subsuming the existing approach.  \nNola is fully mechanized in Rocq as a library of Iris.  \nMoreover, to demonstrate the power of Nola, we develop a prototype of RustHalt, the first semantic and mechanized foundation for total correctness verification of Rust programs.<\/jats:p>","DOI":"10.1145\/3729250","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"98-124","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Nola: Later-Free Ghost State for Verifying Termination in Iris"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5208-3106","authenticated-orcid":false,"given":"Yusuke","family":"Matsushita","sequence":"first","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[{"name":"Chiba University, Chiba, Japan"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_2_2_2_1","volume-title":"Recalling a Witness: Foundations and Applications of Monotonic State. CoRR, abs\/1707.02466","author":"Ahman Danel","year":"2017","unstructured":"Danel Ahman, C\u00e9dric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. 2017. Recalling a Witness: Foundations and Applications of Monotonic State. CoRR, abs\/1707.02466 (2017), arXiv:1707.02466. arxiv:1707.02466"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029818"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.018"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_9"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-017-9431-7"},{"key":"e_1_2_2_16_1","volume-title":"Separation Logic Foundations (Software Foundations","author":"Chargu\u00e9raud Arthur","unstructured":"Arthur Chargu\u00e9raud. 2025. Separation Logic Foundations (Software Foundations, Vol. 6). https:\/\/softwarefoundations.cis.upenn.edu\/slf-current\/ Version 2.3"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_2_2_19_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1958","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall. isbn:013215871X https:\/\/www.worldcat.org\/oclc\/01958445"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591278"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277748"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_9"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607859"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:16)2022"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527326"},{"key":"e_1_2_2_34_1","volume-title":"Understanding and Evolving the Rust Programming Language. Ph. D. Dissertation","author":"Jung Ralf","year":"1880","unstructured":"Ralf Jung. 2020. Understanding and Evolving the Rust Programming Language. Ph. D. Dissertation. Saarland University, Saarbr\u00fccken, Germany. https:\/\/publikationen.sulb.uni-saarland.de\/handle\/20.500.11880\/29647"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591253"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720525"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_2_47_1","volume-title":"CHC-based Program Verification Exploiting Ownership Types","author":"Matsushita Yusuke","unstructured":"Yusuke Matsushita. 2019. CHC-based Program Verification Exploiting Ownership Types. University of Tokyo."},{"key":"e_1_2_2_48_1","volume-title":"Extensible Functional-Correctness Verification of Rust Programs by the Technique of Prophecy. Master\u2019s thesis","author":"Matsushita Yusuke","unstructured":"Yusuke Matsushita. 2021. Extensible Functional-Correctness Verification of Rust Programs by the Technique of Prophecy. Master\u2019s thesis. University of Tokyo."},{"key":"e_1_2_2_49_1","volume-title":"Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows. Ph. D. Dissertation","author":"Matsushita Yusuke","unstructured":"Yusuke Matsushita. 2023. Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows. Ph. D. Dissertation. The University of Tokyo."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","unstructured":"Yusuke Matsushita and Takeshi Tsukada. 2025. Artifact for \u201cNola: Later-Free Ghost State for Verifying Termination in Iris\u201d. https:\/\/doi.org\/10.5281\/zenodo.15190682 10.5281\/zenodo.15190682","DOI":"10.5281\/zenodo.15190682"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_62_1","volume-title":"Using Rust and Creusot to create the world\u2019s fastest deductively verified SAT solver. Master\u2019s thesis","author":"Skot\u00e5m Sarek H\u00f8verstad","unstructured":"Sarek H\u00f8verstad Skot\u00e5m. 2022. CreuSAT, Using Rust and Creusot to create the world\u2019s fastest deductively verified SAT solver. Master\u2019s thesis. University of Oslo. https:\/\/www.duo.uio.no\/handle\/10852\/96757"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177855"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1996.2613"},{"key":"e_1_2_2_76_1","volume-title":"Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis","author":"Ullrich Sebastian","unstructured":"Sebastian Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis. Karlsruhe Institute of Technology."},{"key":"e_1_2_2_77_1","volume-title":"Modular fine-grained concurrency verification. Ph. D. Dissertation","author":"Vafeiadis Viktor","unstructured":"Viktor Vafeiadis. 2008. Modular fine-grained concurrency verification. Ph. D. Dissertation. University of Cambridge, UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.612221"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473597"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:05:02Z","timestamp":1752645902000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729250"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":78,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729250"],"URL":"https:\/\/doi.org\/10.1145\/3729250","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}