{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:04:23Z","timestamp":1784199863385,"version":"3.55.0"},"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. In this paper, we address verification of termination in the presence of advanced features, especially Rust's ownership types. Perhaps surprisingly, this goal cannot be achieved by a simple application of existing studies that dealt only with safety properties. For 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. Even in the presence of advanced features such as invariants and borrows, Nola enables natural termination verification, allowing arbitrary induction in the meta-logic. Its key idea is to parameterize higher-order ghost state, generalizing and subsuming the existing approach. Nola is fully mechanized in Rocq as a library of Iris. Moreover, 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":3,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[{"name":"Chiba University, Chiba, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_2_3_1","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 http:\/\/arxiv.org\/abs\/1707.02466"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029818"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","unstructured":"Vytautas Astrauskas Peter M\u00fcller Federico Poli and Alexander J. Summers. 2019. Leveraging Rust Types for Modular Specification and Verification. Proc. ACM Program. Lang. 3 OOPSLA (2019) 147:1-147:30. doi:10.1145\/3360573","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.018"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_9"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-017-9431-7"},{"key":"e_1_3_2_17_1","volume-title":"Separation Logic Foundations","author":"Chargu\u00e9raud Arthur","year":"2025","unstructured":"Arthur Chargu\u00e9raud. 2025. Separation Logic Foundations. Software Foundations, Vol. 6. https:\/\/softwarefoundations.cis.upenn.edu\/slf-current\/Version2.3."},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_20_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall. https:\/\/www.worldcat.org\/oclc\/01958445"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591278"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277748"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_9"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607859"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:16)2022"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527326"},{"key":"e_1_3_2_35_1","volume-title":"Understanding and Evolving the Rust Programming Language","author":"Jung Ralf","year":"2020","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_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018b. Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. F. Funct. Program. 28 (2018) e20. doi:10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591253"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720525"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_3_2_48_1","unstructured":"Yusuke Matsushita. 2019. CHC-based Program Verification Exploiting Ownership Types. Senior Thesis. University of Tokyo."},{"key":"e_1_3_2_49_1","unstructured":"Yusuke Matsushita. 2021. Extensible Functional-Correctness Verification of Rust Programs by the Technique of Prophecy. Master's thesis. University of Tokyo."},{"key":"e_1_3_2_50_1","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_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_2_52_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. doi:10.5281\/zenodo.15190682","DOI":"10.5281\/zenodo.15190682"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_63_1","unstructured":"Sarek H\u00f8verstad Skot\u00e5m. 2022. CreuSAT Using Rust and Creusot to create the world's fastest deductively verified SAT solver. Master's thesis. University of Oslo. https:\/\/www.duo.uio.no\/handle\/10852\/96757"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177855"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1996.2613"},{"key":"e_1_3_2_77_1","unstructured":"Sebastian Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification. Master's thesis. Karlsruhe Institute of Technology."},{"key":"e_1_3_2_78_1","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_3_2_79_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":[[2026,7,16]],"date-time":"2026-07-16T10:04:12Z","timestamp":1784196252000},"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"}}]}}