{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:47:32Z","timestamp":1780994852150,"version":"3.54.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,8,22]]},"abstract":"<jats:p>Automated deductive program synthesis promises to generate executable programs from concise specifications, along with proofs of correctness that can be independently verified using third-party tools. However, an attempt to exercise this promise using existing proof-certification frameworks reveals significant discrepancies in how proof derivations are structured for two different purposes: program synthesis and program verification. These discrepancies make it difficult to use certified verifiers to validate synthesis results, forcing one to write an ad-hoc translation procedure from synthesis proofs to correctness proofs for each verification backend.<\/jats:p>\n          <jats:p>In this work, we address this challenge in the context of the synthesis and verification of heap-manipulating programs. We present a technique for principled translation of deductive synthesis derivations (a.k.a. source proofs) into deductive target proofs about the synthesised programs in the logics of interactive program verifiers. We showcase our technique by implementing three different certifiers for programs generated via SuSLik, a Separation Logic-based tool for automated synthesis of programs with pointers, in foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST), producing concise and efficient machine-checkable proofs for characteristic synthesis benchmarks.<\/jats:p>","DOI":"10.1145\/3473589","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Certifying the synthesis of heap-manipulating programs"],"prefix":"10.1145","volume":"5","author":[{"given":"Yasunari","family":"Watanabe","sequence":"first","affiliation":[{"name":"Yale-NUS College, Singapore \/ National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kiran","family":"Gopinathan","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"George","family":"P\u00eerlea","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5571-173X","authenticated-orcid":false,"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4250-5392","authenticated-orcid":false,"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"Yale-NUS College, Singapore \/ National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000850"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.012"},{"key":"e_1_2_2_8_1","unstructured":"Fr\u00e9d\u00e9ric Besson and Evgeny Makarov. 2020. Micromega: solvers for arithmetic goals over ordered rings. Online documentation available at https:\/\/coq.inria.fr\/refman\/addendum\/micromega.html  Fr\u00e9d\u00e9ric Besson and Evgeny Makarov. 2020. Micromega: solvers for arithmetic goals over ordered rings. Online documentation available at https:\/\/coq.inria.fr\/refman\/addendum\/micromega.html"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806643"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048147.2048152"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.3"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_7"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44404-1_7"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_2_2_20_1","unstructured":"Georges Gonthier Assia Mahboubi and Enrico Tassi. 2009. A Small Scale Reflection Extension for the Coq system. Microsoft Research \u2013 Inria Joint Centre.  Georges Gonthier Assia Mahboubi and Enrico Tassi. 2009. A Small Scale Reflection Extension for the Coq system. Microsoft Research \u2013 Inria Joint Centre."},{"key":"e_1_2_2_21_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels","author":"Gu Ronghui"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16442-1_14"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_45"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"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_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_5"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4457887"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_2_2_37_1","unstructured":"Alberto Martelli and Ugo Montanari. 1973. Additive AND\/OR Graphs. In IJCAI. William Kaufmann 1\u201311.  Alberto Martelli and Ugo Montanari. 1973. Additive AND\/OR Graphs. In IJCAI. William Kaufmann 1\u201311."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/238721.238781"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277752"},{"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-030-51054-1_7"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018623"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4996238"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363214"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1574"},{"key":"e_1_2_2_52_1","volume-title":"A Framework for Certified Program Synthesis. Master\u2019s thesis","author":"Watanabe Yasunari"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5005829"},{"key":"e_1_2_2_54_1","volume-title":"https:\/\/twitter.com\/IsilDillig\/status\/1287125716761542656 Attributed to Eran Yahav by I\u015fil Dillig in a tweet on","author":"Yahav Eran","year":"2020"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473589","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473589","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473589","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473589"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":53,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473589"],"URL":"https:\/\/doi.org\/10.1145\/3473589","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}