{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:06Z","timestamp":1767928506868,"version":"3.49.0"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","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>\n            The separation logic framework Iris has been built on the premise that all assertions are\n            <jats:italic toggle=\"yes\">stable<\/jats:italic>\n            , meaning they unconditionally enjoy the famous\n            <jats:italic toggle=\"yes\">frame rule<\/jats:italic>\n            . This gives Iris\u2014and the numerous program logics that build on it\u2014very modular reasoning principles. But stability also comes at a cost. It excludes a core feature of the Viper verifier family,\n            <jats:italic toggle=\"yes\">heap-dependent expression assertions<\/jats:italic>\n            , which lift program expressions to the assertion level in order to reduce redundancy between code and specifications and better facilitate SMT-based automation.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we bring heap-dependent expression assertions to Iris with\n            <jats:bold>Daenerys<\/jats:bold>\n            . To do so, we must first revisit the very core of Iris, extending it with a new form of\n            <jats:italic toggle=\"yes\">unstable resources<\/jats:italic>\n            (and adapting the frame rule accordingly). On top, we then build a program logic with heap-dependent expression assertions and lay the foundations for connecting Iris to SMT solvers. We apply Daenerys to several case studies, including some that go beyond what Viper and Iris can do individually and others that benefit from the connection to SMT.\n          <\/jats:p>","DOI":"10.1145\/3729284","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"848-873","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Destabilizing Iris"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5424-9002","authenticated-orcid":false,"given":"Simon","family":"Spies","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-9622-0762","authenticated-orcid":false,"given":"Niklas","family":"M\u00fcck","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2506-3787","authenticated-orcid":false,"given":"Haoyi","family":"Zeng","sequence":"additional","affiliation":[{"name":"Saarland University, Saarland Informatics Campus, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"},{"name":"ISTA, Klosterneuburg, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9303-452X","authenticated-orcid":false,"given":"Andrea","family":"Lattuada","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_2"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel Paul-Andr\u00e9 Melli\u00e8s Christopher D. Richards and J\u00e9r\u00f4me Vouillon. 2007. A very modal model of a modern major general type system. In POPL. ACM 109\u2013122. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-013-9278-5"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9457-5"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","unstructured":"Tej Chajed Joseph Tassarotti M. Frans Kaashoek and Nickolai Zeldovich. 2019. Verifying concurrent crash-safe systems with Perennial. In SOSP. ACM 243\u2013258. https:\/\/doi.org\/10.1145\/3341301.3359632 10.1145\/3341301.3359632","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","unstructured":"Arthur Chargu\u00e9raud. 2011. Characteristic formulae for the verification of imperative programs. In ICFP. ACM 418\u2013430. https:\/\/doi.org\/10.1145\/2034773.2034828 10.1145\/2034773.2034828","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_29"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_10"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_2_17_1","unstructured":"Thibault Dardinier Michael Sammler Gaurav Parthasarathy Alexander J. Summers and Peter M\u00fcller. 2024. Formal Foundations for Translational Separation Logic Verifiers (extended version). arxiv:2407.20002. arxiv:2407.20002"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","unstructured":"Thomas Dinsdale-Young Lars Birkedal Philippa Gardner Matthew J. Parkinson and Hongseok Yang. 2013. Views: compositional reasoning for concurrent programs. In POPL. ACM 287\u2013300. https:\/\/doi.org\/10.1145\/2429069.2429104 10.1145\/2429069.2429104","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477082"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","unstructured":"Derek Dreyer Georg Neis Andreas Rossberg and Lars Birkedal. 2010. A relational modal logic for higher-order stateful ADTs. In POPL. ACM 185\u2013198. https:\/\/doi.org\/10.1145\/1706299.1706323 10.1145\/1706299.1706323","DOI":"10.1145\/1706299.1706323"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_33"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In LICS. ACM 442\u2013451. https:\/\/doi.org\/10.1145\/3209108.3209174 10.1145\/3209108.3209174","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_27_1","volume-title":"Understanding and Evolving the Rust Programming Language. Ph. D. Dissertation","author":"Jung Ralf","unstructured":"Ralf Jung. 2020. Understanding and Evolving the Rust Programming Language. Ph. D. Dissertation. Saarland University."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. ACM 256\u2013269. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547628"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. ACM 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_23"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571194"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_29"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_2_2_49_1","volume-title":"Redis Pocount Implementation for Potentially Large Buffers. https:\/\/github.com\/redis\/redis\/blob\/3fac869f02657d94dc89fab23acb8ef188889c96\/src\/bitops.c#L40","unstructured":"Redis. 2024. Redis Pocount Implementation for Potentially Large Buffers. https:\/\/github.com\/redis\/redis\/blob\/3fac869f02657d94dc89fab23acb8ef188889c96\/src\/bitops.c#L40"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_51_1","unstructured":"Rocq. 2025. The Rocq Prover. https:\/\/rocq-prover.org"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: Automating the foundational verification of C code with refined ownership types. In PLDI. ACM 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","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","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","unstructured":"Simon Spies Niklas M\u00fcck Haoyi Zeng Michael Sammler Andrea Lattuada Peter M\u00fcller and Derek Dreyer. 2025. Destabilizing Iris (Rocq development and appendix). https:\/\/doi.org\/10.5281\/zenodo.15041581 Project webpage: 10.5281\/zenodo.15041581","DOI":"10.5281\/zenodo.15041581"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024. A Logical Approach to Type Soundness. J. ACM July issn:0004-5411 https:\/\/doi.org\/10.1145\/3676954 10.1145\/3676954","DOI":"10.1145\/3676954"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","unstructured":"Aaron Turon Derek Dreyer and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP. ACM 377\u2013390. https:\/\/doi.org\/10.1145\/2500365.2500600 10.1145\/2500365.2500600","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3703595.3705876"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428296"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_17"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563345"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729284","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:06:16Z","timestamp":1752645976000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729284"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":66,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729284"],"URL":"https:\/\/doi.org\/10.1145\/3729284","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","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"}}]}}