Abstract: In program synthesis there is a well-known trade-off between concise and strong 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's 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 read-only borrows. We observe that this minimalistic and conservative SSL extension benefits the synthesis in several ways, making it more (a) expressive (stronger correctness guarantees are achieved with a modest annotation overhead), (b) effective (it produces more concise and easier-to-read programs), (c) efficient (faster synthesis), and (d) robust (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)--(d) by describing our quantitative evaluation of the borrowing-aware synthesis implementation on a series of standard benchmark specifications for various heap-manipulating programs.

Bio: Andreea is a Research Fellow at School of Computing, National University of Singapore, where she also received her PhD from in 2018. Her research interests span across different programming languages topics such as software verification (in particular separation logic flavoured), program synthesis, and concurrent program repair.

NB! This seminar is done over Zoom from Singapore during the weekly SPG Research Group time slot:

https://ecs.wgtn.ac.nz/Groups/SPG/WebHome

Join over Zoom - email Alex Potanin (alex@ecs.vuw.ac.nz) to ask for the Zoom link. Thanks!