{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:44Z","timestamp":1780994804454,"version":"3.54.1"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"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":[[2019,1,2]]},"abstract":"<jats:p>\n            This paper describes a deductive approach to synthesizing imperative programs with pointers from declarative specifications expressed in Separation Logic. Our synthesis algorithm takes as input a pair of assertions\u2014a pre- and a postcondition\u2014which describe two states of the symbolic heap, and derives a program that transforms one state into the other, guided by the shape of the heap. Our approach to program synthesis is grounded in proof theory: we introduce the novel framework of Synthetic Separation Logic (SSL), which generalises the classical notion of heap entailment\n            <jats:italic>P<\/jats:italic>\n            \u22a2\n            <jats:italic>Q<\/jats:italic>\n            to incorporate a possibility of transforming a heap satisfying an assertion\n            <jats:italic>P<\/jats:italic>\n            into a heap satisfying an assertion\n            <jats:italic>Q<\/jats:italic>\n            . A synthesized program represents a proof term for a transforming entailment statement\n            <jats:italic>P<\/jats:italic>\n            \u219d\n            <jats:italic>Q<\/jats:italic>\n            , and the synthesis procedure corresponds to a proof search. The derived programs are, thus, correct by construction, in the sense that they satisfy the ascribed pre\/postconditions, and are accompanied by complete proof derivations, which can be checked independently.\n          <\/jats:p>\n          <jats:p>We have implemented a proof search engine for SSL in a form of the program synthesizer called SuSLik. For efficiency, the engine exploits properties of SSL rules, such as invertibility and commutativity of rule applications on separate heaps, to prune the space of derivations it has to consider. We explain and showcase the use of SSL on characteristic examples, describe the design of SuSLik, and report on our experience of using it to synthesize a series of benchmark programs manipulating heap-based linked data structures.<\/jats:p>","DOI":"10.1145\/3290385","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":43,"title":["Structuring the synthesis of heap-manipulating programs"],"prefix":"10.1145","volume":"3","author":[{"given":"Nadia","family":"Polikarpova","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"CAV (Part II) (LNCS)","author":"Albarghouthi Aws"},{"key":"e_1_2_2_2_1","volume-title":"Syntax-guided synthesis","author":"Alur Rajeev"},{"key":"e_1_2_2_3_1","volume-title":"TACAS (Part I) (LNCS)","author":"Alur Rajeev"},{"key":"e_1_2_2_4_1","volume-title":"FOSSACS (LNCS)","author":"Antonopoulos Timos"},{"key":"e_1_2_2_5_1","volume-title":"ESOP (LNCS)","author":"Appel Andrew W."},{"key":"e_1_2_2_6_1","volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_2_10_1","volume-title":"CAV (LNCS)","author":"Berdine Josh"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_14"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328453"},{"key":"e_1_2_2_13_1","volume-title":"Kanovich","author":"Brotherston James","year":"2017"},{"key":"e_1_2_2_14_1","volume-title":"APLAS (LNCS)","author":"Brotherston James"},{"key":"e_1_2_2_15_1","volume-title":"Infer: An Automatic Program Verifier for Memory Safety of C Programs. In NASA Formal Methods (LNCS)","author":"Calcagno Cristiano","year":"2011"},{"key":"e_1_2_2_16_1","volume-title":"Appel","author":"Cao Qinxiang","year":"2017"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136000.3136004"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863590"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048147.2048152"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_2_23_1","unstructured":"Coq Development Team. 2018. The Coq Proof Assistant Reference Manual - Version 8.8. Available at http:\/\/coq.inria.fr\/ .  Coq Development Team. 2018. The Coq Proof Assistant Reference Manual - Version 8.8. Available at http:\/\/coq.inria.fr\/ ."},{"key":"e_1_2_2_24_1","volume-title":"TACAS (LNCS)","author":"de Moura Leonardo Mendon\u00e7a"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"Shingo Eguchi Naoki Kobayashi and Takeshi Tsukada. 2018. Automated Synthesis of Functional Programs with Auxiliary Functions. In APLAS. To appear.  Shingo Eguchi Naoki Kobayashi and Takeshi Tsukada. 2018. Automated Synthesis of Functional Programs with Auxiliary Functions. In APLAS. To appear.","DOI":"10.1007\/978-3-030-02768-1_13"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837629"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034798"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983993"},{"key":"e_1_2_2_35_1","volume-title":"Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods (LNCS)","author":"Jacobs Bart"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_8"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050057"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806632"},{"key":"e_1_2_2_40_1","volume-title":"ICFEM (LNCS)","author":"Le Ton Chanh"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594333"},{"key":"e_1_2_2_42_1","volume-title":"ESOP (LNCS)","author":"Le Xuan Bach"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_2_44_1","unstructured":"K. Rustan M. Leino. 2013. Developing verified programs with Dafny. In ICSE. ACM 1488\u20131490.   K. Rustan M. Leino. 2013. Developing verified programs with Dafny. In ICSE. ACM 1488\u20131490."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384646"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103673"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_2_2_49_1","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis.  Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_24"},{"key":"e_1_2_2_51_1","unstructured":"Chris Mellish and Steve Hardy. 1984. Integrating Prolog in the POPLOG Environment. In Implementations of Prolog. 147\u2013162.  Chris Mellish and Steve Hardy. 1984. Integrating Prolog in the POPLOG Environment. In Implementations of Prolog. 147\u2013162."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158089"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_54_1","unstructured":"Vijayaraghavan Murali Letao Qi Swarat Chaudhuri and Chris Jermaine. 2018. Neural Sketch Learning for Conditional Program Generation. In ICLR. To appear.  Vijayaraghavan Murali Letao Qi Swarat Chaudhuri and Chris Jermaine. 2018. Neural Sketch Learning for Conditional Program Generation. In ICLR. To appear."},{"key":"e_1_2_2_55_1","volume-title":"Separation Logic and Concurrency. (June","author":"Nanevski Aleksandar","year":"2016"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_2_2_57_1","volume-title":"VMCAI (LNCS)","author":"Nguyen Huu Hai"},{"key":"e_1_2_2_58_1","volume-title":"CSL (LNCS)","author":"O\u2019Hearn Peter W."},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498929"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_2_2_61_1","volume-title":"Lecture Notes on Focusing. (June","author":"Pfenning Frank","year":"2010"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_2_2_63_1","volume-title":"TACAS (LNCS)","author":"Piskac Ruzica"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814310"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133889"},{"key":"e_1_2_2_69_1","volume-title":"Barrett","author":"Reynolds Andrew","year":"2015"},{"key":"e_1_2_2_70_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures","author":"Reynolds John C.","year":"2002"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018623"},{"key":"e_1_2_2_72_1","volume-title":"SNAPL (LIPIcs)","volume":"71","author":"Scherer Gabriel","year":"2017"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236034"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908102"},{"key":"e_1_2_2_75_1","volume-title":"SAS (LNCS)","author":"So Sunbeom"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180250"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133887"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290385","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290385","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290385"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":80,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290385"],"URL":"https:\/\/doi.org\/10.1145\/3290385","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}