{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:54:35Z","timestamp":1770288875183,"version":"3.49.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1901033"],"award-info":[{"award-number":["CCF-1901033"]}],"id":[{"id":"10.13039\/100000001","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":[[2024,1,2]]},"abstract":"<jats:p>Gradual verification, which supports explicitly partial specifications and verifies them with a combination of static and dynamic checks, makes verification more incremental and provides earlier feedback to developers. While an abstract, weakest precondition-based approach to gradual verification was previously proven sound, the approach did not provide sufficient guidance for implementation and optimization of the required run-time checks. More recently, gradual verification was implemented using symbolic execution techniques, but the soundness of the approach (as with related static checkers based on implicit dynamic frames) was an open question. This paper puts practical gradual verification on a sound footing with a formalization of symbolic execution, optimized run-time check generation, and run time execution. We prove our approach is sound; our proof also covers a core subset of the Viper tool, for which we are aware of no previous soundness result. Our formalization enabled us to find a soundness bug in an implemented gradual verification tool and describe the fix necessary to make it sound.<\/jats:p>","DOI":"10.1145\/3632927","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2547-2576","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Sound Gradual Verification with Symbolic Execution"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3961-3043","authenticated-orcid":false,"given":"Conrad","family":"Zimmerman","sequence":"first","affiliation":[{"name":"Brown University, Providence, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3029-2617","authenticated-orcid":false,"given":"Jenna","family":"DiVincenzo","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0631-5591","authenticated-orcid":false,"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","volume-title":"Department of Computer Science","author":"Arnold. Rob","year":"2010","unstructured":"Rob Arnold. 2010. C0, an Imperative Programming Language for Novice Computer Scientists. Master\u2019s thesis. Department of Computer Science, Carnegie Mellon University. http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/anon\/usr\/ftp\/home\/ftp\/2010\/CMU-CS-10-145.pdf"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-03106773-0_5"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_2"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449955.1449782"},{"key":"e_1_3_1_8_1","unstructured":"Jenna DiVincenzo Ian McCormack Hemant Gouni Jacob Gorenburg Mona Zhang Conrad Zimmerman Joshua Sunshine \u00c9ric Tanter and Jonathan Aldrich. 2022. Gradual C0: Symbolic Execution for Efficient Gradual Verification. arXiv:2210.02428 [cs.LO]"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_33"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Ronald Garcia Alison M. Clark and \u00c9ric Tanter. 2016. Abstracting Gradual Typing. (2016) 429\u2013442. https:\/\/doi.org\/10.1145\/2837614.2837670 10.1145\/2837614.2837670","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_2"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3642-20398-5_4"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547628"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806645"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040326"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_33"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.3929\/ETHZ-A-010835519"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_6"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-95891-8_51"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1774088.1774610"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:19)2015"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428296"},{"key":"e_1_3_1_31_1","doi-asserted-by":"crossref","unstructured":"Conrad Zimmerman Jenna DiVincenzo and Jonathan Aldrich. 2024. Sound Gradual Verification with Symbolic Execution. (2024). arXiv:2311.07559 [cs.PL]","DOI":"10.1145\/3632927"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632927","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632927","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632927","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:05:31Z","timestamp":1751659531000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632927"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":30,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632927"],"URL":"https:\/\/doi.org\/10.1145\/3632927","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}