{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:08:40Z","timestamp":1790075320836,"version":"4.0.1"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,6,8]]},"abstract":"<jats:p>\n                    The CCR framework unifies refinement and separation logic to provide ownership-based modular reasoning and transitive incremental reasoning in open settings that involve unverified code. However, when reasoning about function invocations, the reasoning principles available to clients remain confined to pre- and postconditions, which struggle to capture effectful behaviors such as I\/O actions or interactions with arbitrary unverified code. This limitation becomes particularly acute in\n                    <jats:italic toggle=\"yes\">hybrid verification<\/jats:italic>\n                    , where a mixture of different verification techniques is applied and some code is never formally verified but instead tested or model-checked.\n                  <\/jats:p>\n                  <jats:p>\n                    To overcome this limitation, we introduce\n                    <jats:italic toggle=\"yes\">imaginary specifications<\/jats:italic>\n                    \u2014a novel notion that freely mixes executable code with ownership assertions\u2014and reasoning principles for their use. Through key technical developments, we present CRIS (Contextual Refinement with Imaginary Specifications), a framework that generalizes CCR with support for imaginary specifications. We demonstrate CRIS\u2019s expressiveness and reasoning power through examples involving hybrid verification with unverified code exhibiting arbitrary side effects such as I\/O or divergence, with complete mechanization in Rocq.\n                  <\/jats:p>","DOI":"10.1145\/3808317","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"1764-1787","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["CRIS: The Power of Imagination in Hybrid Verification"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-6455-3491","authenticated-orcid":false,"given":"Yonghee","family":"Kim","sequence":"first","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0035-4077","authenticated-orcid":false,"given":"Taeyoung","family":"Yoon","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-0931-2102","authenticated-orcid":false,"given":"Sanghyun","family":"Yi","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6423-9561","authenticated-orcid":false,"given":"Jaehyung","family":"Lee","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2750-5221","authenticated-orcid":false,"given":"Soonwon","family":"Moon","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6331-2335","authenticated-orcid":false,"given":"Yeji","family":"Han","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7757-5580","authenticated-orcid":false,"given":"Seonho","family":"Lee","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9180-6357","authenticated-orcid":false,"given":"Taeyoung","family":"Rhee","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4434-3973","authenticated-orcid":false,"given":"Yujin","family":"Im","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-4254-1795","authenticated-orcid":false,"given":"Donghyun","family":"Nam","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7581-041X","authenticated-orcid":false,"given":"Jieung","family":"Kim","sequence":"additional","affiliation":[{"name":"Yonsei University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1656-0913","authenticated-orcid":false,"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987212"},{"key":"e_1_3_1_3_2","volume-title":"Refinement calculus: a systematic introduction","author":"Back Ralph-Johan","year":"2012","unstructured":"Ralph-Johan Back and Joakim Wright. 2012. Refinement calculus: a systematic introduction. Springer Science & Business Media."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/648216.750907"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622857"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3776676"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706323"},{"key":"e_1_3_1_9_2","doi-asserted-by":"crossref","unstructured":"M. Eilers M. Schwerhoff A. J. Summers and P. M\u00fcller. 2025. Fifteen Years of Viper. In Computer Aided Verification (CAV). To appear.","DOI":"10.1007\/978-3-031-98668-0_5"},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. ReLoC: A mechanised relational logic for fine-grained concurrency. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. 442\u2013451.","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192381"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429093"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_17_2","article-title":"Featherweight verifast","volume":"11","author":"Jacobs Bart","year":"2015","unstructured":"Bart Jacobs, Fr\u00e9d\u00e9ric Vogels, and Frank Piessens. 2015. Featherweight verifast. Logical Methods in Computer Science 11 (2015).","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Yonghee Kim Taeyoung Yoon Sanghyun Yi Jaehyung Lee Soonwon Moon Yeji Han Seonho Lee Taeyoung Rhee Yujin Im Donghyun Nam Jieung Kim and Chung-Kil Hur. 2026. Artifact for CRIS: The Power of Imagination in Hybrid Verification (PLDI 2026 Artifact). doi: 10.5281\/zenodo.19491861","DOI":"10.5281\/zenodo.19491861"},{"key":"e_1_3_1_21_2","doi-asserted-by":"crossref","unstructured":"J\u00e9r\u00e9mie Koenig. 2020. Refinement-Based Game Semantics for Certified Components. https:\/\/flint.cs.yale.edu\/flint\/publications\/koenig-phd.pdf","DOI":"10.1145\/3373718.3394799"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394799"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_22"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571220"},{"key":"e_1_3_1_29_2","unstructured":"Youngju Song and Minki Cho. 2025. CCR 2.0: High-level Reasoning for Conditional Refinements. arXiv:2507.04298 [cs.PL] https:\/\/arxiv.org\/abs\/2507.04298"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_1_31_2","doi-asserted-by":"crossref","unstructured":"Aaron Turon Derek Dreyer and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In Proceedings of the 18th ACM SIGPLAN international conference on Functional programming. 377\u2013390.","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373813"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632914"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704900"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808317","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:49:51Z","timestamp":1790074191000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808317"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":35,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808317"],"URL":"https:\/\/doi.org\/10.1145\/3808317","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}