{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:04:56Z","timestamp":1767927896130,"version":"3.49.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030449131","type":"print"},{"value":"9783030449148","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T00:00:00Z","timestamp":1587168000000},"content-version":"vor","delay-in-days":108,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In program synthesis there is a well-known trade-off between <jats:italic>concise<\/jats:italic> and <jats:italic>strong<\/jats:italic> specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the user\u2019s intent. In this work we explore the use of annotations for restricting memory access permissions in program synthesis, and show that they can make specifications much stronger while remaining surprisingly concise. Specifically, we enhance Synthetic Separation Logic (SSL), a framework for synthesis of heap-manipulating programs, with the logical mechanism of <jats:italic>read-only borrows<\/jats:italic>.<\/jats:p><jats:p>We observe that this minimalistic and conservative SSL extension benefits the synthesis in several ways, making it more (a)\u00a0<jats:italic>expressive<\/jats:italic> (stronger correctness guarantees are achieved with a modest annotation overhead), (b)\u00a0<jats:italic>effective<\/jats:italic> (it produces more concise and easier-to-read programs), (c)\u00a0<jats:italic>efficient<\/jats:italic> (faster synthesis), and (d)\u00a0<jats:italic>robust<\/jats:italic> (synthesis efficiency is less affected by the choice of the search heuristic). We explain the intuition and provide formal treatment for read-only borrows. We substantiate the claims (a)\u2013(d) by describing our quantitative evaluation of the borrowing-aware synthesis implementation on a series of standard benchmark specifications for various heap-manipulating programs.<\/jats:p>","DOI":"10.1007\/978-3-030-44914-8_6","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"141-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Concise Read-Only Specifications for Better Synthesis of Programs with Pointers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9089-9392","authenticated-orcid":false,"given":"Andreea","family":"Costea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5766-7090","authenticated-orcid":false,"given":"Amy","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5571-173X","authenticated-orcid":false,"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4250-5392","authenticated-orcid":false,"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,18]]},"reference":[{"key":"6_CR1","unstructured":"The Rust Programming Language: References and Borrowing. https:\/\/doc.rust-lang.org\/1.8.0\/book\/references-and-borrowing.html, 2019."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Rastislav Bod\u00edk, Garvit Juniwal, Milo M.\u00a0K. Martin, Mukund Raghothaman, Sanjit\u00a0A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In FMCAD, pages 1\u20138. IEEE, 2013.","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Andrew\u00a0W. Appel. Verified software toolchain - (invited talk). In ESOP, volume 6602 of LNCS, pages 1\u201317. Springer, 2011.","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Vytautas Astrauskas, Peter M\u00fcller, Federico Poli, and Alexander\u00a0J. Summers. Leveraging Rust types for modular specification and verification. PACMPL, 3(OOPSLA):147:1\u2013147:30, 2019.","DOI":"10.1145\/3360573"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Thibaut Balabonski, Fran\u00e7ois Pottier, and Jonathan Protzenko. The Design and Formalization of Mezzo, a Permission-Based Programming Language. ACM Trans. Program. Lang. Syst., 38(4):14:1\u201314:94, 2016.","DOI":"10.1145\/2837022"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Josh Berdine, Cristiano Calcagno, and Peter\u00a0W. O\u2019Hearn. Symbolic execution with separation logic. In APLAS, volume 3780 of LNCS, pages 52\u201368. Springer, 2005.","DOI":"10.1007\/11575467_5"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Richard Bornat, Cristiano Calcagno, Peter\u00a0W. O\u2019Hearn, and Matthew\u00a0J. Parkinson. Permission Accounting in Separation Logic. In POPL, pages 259\u2013270. ACM, 2005.","DOI":"10.1145\/1047659.1040327"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"John Boyland. Checking Interference with Fractional Permissions. In SAS, volume 2694 of LNCS, pages 55\u201372. Springer, 2003.","DOI":"10.1007\/3-540-44898-5_4"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. Temporary Read-Only Permissions for Separation Logic. In ESOP, volume 10201 of LNCS, pages 260\u2013286. Springer, 2017.","DOI":"10.1007\/978-3-662-54434-1_10"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Dave Clarke, Johan \u00d6stlund, Ilya Sergey, and Tobias Wrigstad. Ownership Types: A Survey, pages 15\u201358. Springer Berlin Heidelberg, 2013.","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Andreea Costea, Asankhaya Sharma, and Cristina David. HIPimm: verifying granular immutability guarantees. In PEPM, pages 189\u2013194. ACM, 2014.","DOI":"10.1145\/2543728.2543743"},{"key":"6_CR12","unstructured":"Andreea Costea, Amy Zhu, Nadia Polikarpova, and Ilya Sergey. ROBoSuSLik: ESOP 2020 Artifact. 2020. DOI: 10.5281\/zenodo.3630044."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Cristina David and Wei-Ngan Chin. Immutable specifications for more concise and precise verification. In OOPSLA, pages 359\u2013374. ACM, 2011.","DOI":"10.1145\/2076021.2048096"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Benjamin Delaware, Cl\u00e9ment Pit-Claudel, Jason Gross, and Adam Chlipala. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. In POPL, pages 689\u2013700. ACM, 2015.","DOI":"10.1145\/2775051.2677006"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Robert Dockins, Aquinas Hobor, and Andrew\u00a0W. Appel. A fresh look at separation algebras and share accounting. In APLAS, volume 5904 of LNCS, pages 161\u2013177. Springer, 2009.","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Ronald Garcia, \u00c9ric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst., 36(4):12:1\u201312:44, 2014.","DOI":"10.1145\/2629609"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Adri\u00e0 Gasc\u00f3n, Ashish Tiwari, Brent Carmer, and Umang Mathur. Look for the proof to find the program: Decorated-component-based program synthesis. In CAV, volume 10427 of LNCS, pages 86\u2013103. Springer, 2017.","DOI":"10.1007\/978-3-319-63390-9_5"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Colin\u00a0S. Gordon, Matthew\u00a0J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Uniqueness and reference immutability for safe parallelism. In OOPSLA, pages 21\u201340. ACM, 2012.","DOI":"10.1145\/2398857.2384619"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. Synthesis of loop-free programs. In PLDI, pages 62\u201373. ACM, 2011.","DOI":"10.1145\/1993316.1993506"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Stefan Heule, K.\u00a0Rustan\u00a0M. Leino, Peter M\u00fcller, and Alexander\u00a0J. Summers. Abstract read permissions: Fractional permissions without the fractions. In VMCAI, volume 7737 of LNCS, pages 315\u2013334. Springer, 2013.","DOI":"10.1007\/978-3-642-35873-9_20"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Bart Jacobs, Jan Smans, Pieter Philippaerts, Fr\u00e9d\u00e9ric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods, volume 6617 of LNCS, pages41\u201355. Springer, 2011.","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the foundations of the Rust programming language. PACMPL, 2(POPL):66, 2017.","DOI":"10.1145\/3158154"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. Synthesis modulo recursive functions. In OOPSLA, pages 407\u2013426. ACM, 2013.","DOI":"10.1145\/2544173.2509555"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Tristan Knoth, Di\u00a0Wang, Nadia Polikarpova, and Jan Hoffmann. Resource-guided program synthesis. In PLDI, pages 253\u2013268. ACM, 2019.","DOI":"10.1145\/3314221.3314602"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Xuan\u00a0Bach Le and Aquinas Hobor. Logical reasoning for disjoint permissions. In ESOP, volume 10801 of LNCS, pages 385\u2013414. Springer, 2018.","DOI":"10.1007\/978-3-319-89884-1_14"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"K.\u00a0Rustan\u00a0M. Leino and Aleksandar Milicevic. Program Extrapolation with Jennisys. In OOPSLA, pages 411\u2013430. ACM, 2012.","DOI":"10.1145\/2398857.2384646"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"K.\u00a0Rustan\u00a0M. Leino and Peter M\u00fcller. A Basis for Verifying Multi-threaded Programs. In ESOP, volume 5502 of LNCS, pages 378\u2013393. Springer, 2009.","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"K.\u00a0Rustan\u00a0M. Leino, Peter M\u00fcller, and Jan Smans. Verification of Concurrent Programs with Chalice. In Foundations of Security Analysis and Design V, FOSAD2007\/2008\/2009 Tutorial Lectures, volume 5705 of LNCS, pages 195\u2013222. Springer, 2009.","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Zohar Manna and Richard\u00a0J. Waldinger. A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst., 2(1):90\u2013121, 1980.","DOI":"10.1145\/357084.357090"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander\u00a0J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. In VMCAI, volume 9583 of LNCS, pages 41\u201362. Springer, 2016.","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Karl Naden, Robert Bocchino, Jonathan Aldrich, and Kevin Bierhoff. A type system for borrowing permissions. In POPL, pages 557\u2013570. ACM, 2012.","DOI":"10.1145\/2103621.2103722"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Peter\u00a0W. O\u2019Hearn, John\u00a0C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL, volume 2142 of LNCS, pages 1\u201319. Springer, 2001.","DOI":"10.1007\/3-540-44802-0_1"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. Program synthesis from polymorphic refinement types. In PLDI, pages 522\u2013538. ACM, 2016.","DOI":"10.1145\/2980983.2908093"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Nadia Polikarpova and Ilya Sergey. Structuring the Synthesis of Heap-Manipulating Programs. PACMPL, 3(POPL):72:1\u201372:30, 2019.","DOI":"10.1145\/3290385"},{"key":"6_CR35","unstructured":"Nadia Polikarpova, Jean Yang, Shachar Itzhaky, and Armando Solar-Lezama. Enforcing information flow policies with type-targeted program synthesis. CoRR, abs\/1607.03445, 2016."},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Xiaokang Qiu and Armando Solar-Lezama. Natural synthesis of provably-correct data-structure manipulations.PACMPL, 1(OOPSLA):65:1\u201365:28, 2017.","DOI":"10.1145\/3133889"},{"key":"6_CR37","unstructured":"John\u00a0C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55\u201374. IEEE Computer Society, 2002."},{"key":"6_CR38","unstructured":"Reuben N.\u00a0S. Rowe and James Brotherston. Automatic cyclic termination proofs for recursive procedures in separation logic. In CPP, pages 53\u201365. ACM, 2017."},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Calvin Smith and Aws Albarghouthi. Synthesizing differentially private programs. Proc. ACM Program. Lang., 3(ICFP):94:1\u201394:29, July 2019.","DOI":"10.1145\/3341698"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama. Program sketching. STTT, 15(5-6):475\u2013495, 2013.","DOI":"10.1007\/s10009-012-0249-7"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Saurabh Srivastava, Sumit Gulwani, and Jeffrey\u00a0S. Foster. From program verification to program synthesis. In POPL, pages 313\u2013326. ACM, 2010.","DOI":"10.1145\/1707801.1706337"},{"key":"6_CR42","doi-asserted-by":"crossref","unstructured":"Sven Stork, Karl Naden, Joshua Sunshine, Manuel Mohr, Alcides Fonseca, Paulo Marques, and Jonathan Aldrich. \u00c6minium: A Permission-Based Concurrent-by-Default Programming Language Approach.TOPLAS, 36(1):2:1\u20132:42, 2014.","DOI":"10.1145\/2543920"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Alexander\u00a0J. Summers and Peter M\u00fcller. Automating deductive verification for weak-memory programs. In TACAS, volume 10805 of LNCS, pages 190\u2013209. Springer, 2018.","DOI":"10.1007\/978-3-319-89960-2_11"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"Emina Torlak and Rastislav Bod\u00edk. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI, pages 530\u2013541. ACM, 2014.","DOI":"10.1145\/2666356.2594340"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-44914-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,30]],"date-time":"2022-06-30T17:10:16Z","timestamp":1656609016000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-44914-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030449131","9783030449148"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-44914-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"18 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11-12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}