{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:19:06Z","timestamp":1783009146105,"version":"3.54.5"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004750","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1901033,DGE1745016"],"award-info":[{"award-number":["CCF-1901033,DGE1745016"]}],"id":[{"id":"10.13039\/501100004750","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":[[2020,11,13]]},"abstract":"<jats:p>Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, prior work proposed gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. The prior approach to gradual verification, however, was limited to programs without recursive data structures. This paper extends gradual verification to programs that manipulate recursive, mutable data structures on the heap. We address several technical challenges, such as semantically connecting iso- and equi-recursive interpretations of abstract predicates, and supporting gradual verification of heap ownership. This work thus lays the foundation for future tools that work on realistic programs and support verification within an engineering process in which cost-benefit trade-offs can be made.<\/jats:p>","DOI":"10.1145\/3428296","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:40:14Z","timestamp":1606261214000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Gradual verification of recursive heap data structures"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3029-2617","authenticated-orcid":false,"given":"Jenna","family":"Wise","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Johannes","family":"Bader","sequence":"additional","affiliation":[{"name":"Jane Street, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cameron","family":"Wong","sequence":"additional","affiliation":[{"name":"Jane Street, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0631-5591","authenticated-orcid":false,"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9672-5297","authenticated-orcid":false,"given":"Joshua","family":"Sunshine","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Gradual Program Verification. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 25-46","author":"Bader Johannes","year":"2018","unstructured":"Johannes Bader , Jonathan Aldrich , and \u00c9ric Tanter . 2018 . Gradual Program Verification. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 25-46 . Johannes Bader, Jonathan Aldrich, and \u00c9ric Tanter. 2018. Gradual Program Verification. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 25-46."},{"key":"e_1_2_2_2_1","volume-title":"International Symposium on Formal Methods for Components and Objects. Springer, 115-137","author":"Berdine Josh","year":"2005","unstructured":"Josh Berdine , Cristiano Calcagno , and Peter W O'hearn . 2005 . Smallfoot: Modular automatic assertion checking with separation logic . In International Symposium on Formal Methods for Components and Objects. Springer, 115-137 . Josh Berdine, Cristiano Calcagno, and Peter W O'hearn. 2005. Smallfoot: Modular automatic assertion checking with separation logic. In International Symposium on Formal Methods for Components and Objects. Springer, 115-137."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Dino Distefano and Matthew J Parkinson J. 2008. jStar: Towards practical verification for Java. ACM Sigplan Notices 43 10 ( 2008 ) 213-226.  Dino Distefano and Matthew J Parkinson J. 2008. jStar: Towards practical verification for Java. ACM Sigplan Notices 43 10 ( 2008 ) 213-226.","DOI":"10.1145\/1449955.1449782"},{"key":"e_1_2_2_5_1","volume-title":"Fields of logic and computation","author":"Furia Carlo Alberto","unstructured":"Carlo Alberto Furia and Bertrand Meyer . 2010. Inferring loop invariants using postconditions . In Fields of logic and computation . Springer , 277-300. Carlo Alberto Furia and Bertrand Meyer. 2010. Inferring loop invariants using postconditions. In Fields of logic and computation. Springer, 277-300."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Ronald Garcia \u00c9ric Tanter Roger Wolf and Jonathan Aldrich. 2014. Foundations of Typestate-Oriented Programming. 36 4 Article 12 (Oct. 2014 ) 12 : 1-12 :44 pages.  Ronald Garcia \u00c9ric Tanter Roger Wolf and Jonathan Aldrich. 2014. Foundations of Typestate-Oriented Programming. 36 4 Article 12 (Oct. 2014 ) 12 : 1-12 :44 pages.","DOI":"10.1145\/2629609"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12 10 ( 1969 ) 576-580.  Charles Antony Richard Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12 10 ( 1969 ) 576-580.","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_9_1","first-page":"775","volume-title":"Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017 )","author":"Nico","unstructured":"Nico Lehmann and \u00c9ric Tanter. 2017. Gradual Refinement Types . In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017 ) . Paris, France , 775 - 788 . Nico Lehmann and \u00c9ric Tanter. 2017. Gradual Refinement Types. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017 ). Paris, France, 775-788."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_2_11_1","volume-title":"Verification of concurrent programs with Chalice","author":"Leino K Rustan M","unstructured":"K Rustan M Leino , Peter M\u00fcller , and Jan Smans . 2009. Verification of concurrent programs with Chalice . In Foundations of Security Analysis and Design V. Springer , 195-222. K Rustan M Leino, Peter M\u00fcller, and Jan Smans. 2009. Verification of concurrent programs with Chalice. In Foundations of Security Analysis and Design V. Springer, 195-222."},{"key":"e_1_2_2_12_1","unstructured":"Paqui Lucio. 2017. A Tutorial on Using Dafny to Construct Verified Software. arXiv preprint arXiv:1701.04481 ( 2017 ).  Paqui Lucio. 2017. A Tutorial on Using Dafny to Construct Verified Software. arXiv preprint arXiv:1701.04481 ( 2017 )."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78163-9_19"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_2_15_1","unstructured":"Guillaume Petiot Nikolai Kosmatov Alain Giorgetti and Jacques Julliand. 2014. StaDy: Deep Integration of Static and Dynamic Analysis in Frama-C. ( 2014 ).  Guillaume Petiot Nikolai Kosmatov Alain Giorgetti and Jacques Julliand. 2014. StaDy: Deep Integration of Static and Dynamic Analysis in Frama-C. ( 2014 )."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_29"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_2_2_19_1","first-page":"81","volume-title":"Scheme and Functional Programming Workshop","volume":"6","author":"Siek Jeremy G","year":"2006","unstructured":"Jeremy G Siek and Walid Taha . 2006 . Gradual typing for functional languages . In Scheme and Functional Programming Workshop , Vol. 6 . 81 - 92 . Jeremy G Siek and Walid Taha. 2006. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, Vol. 6. 81-92."},{"key":"e_1_2_2_20_1","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics","volume":"32","author":"Siek Jeremy G","year":"2015","unstructured":"Jeremy G Siek , Michael M Vitousek , Matteo Cimini , and John Tang Boyland . 2015 . Refined criteria for gradual typing . In LIPIcs-Leibniz International Proceedings in Informatics , Vol. 32 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Jeremy G Siek, Michael M Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics, Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_6"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4085932"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22655-7_22"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428296","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428296","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:58Z","timestamp":1750197778000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428296"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":24,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428296"],"URL":"https:\/\/doi.org\/10.1145\/3428296","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}