Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 09:00 - 09:22 at Sala II - Synthesis Chair(s): Robbert Krebbers

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—a pre- and a postcondition— which 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 $P \vdash Q$ to incorporate a possibility of transforming a heap satisfying an assertion $P$ into a heap satisfying an assertion $Q$. A synthesized program represents a proof term for a transforming entailment statement $P \leadsto Q$, 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.

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.

Slides (suslik-popl19.pdf)8.14MiB

Thu 17 Jan

POPL-2019-Research-Papers
09:00 - 10:06: Research Papers - Synthesis at Sala II
Chair(s): Robbert KrebbersDelft University of Technology
POPL-2019-Research-Papers09:00 - 09:22
Talk
Nadia PolikarpovaUniversity of California, San Diego, Ilya SergeyYale-NUS College and National University of Singapore
Link to publication DOI Pre-print Media Attached File Attached
POPL-2019-Research-Papers09:22 - 09:44
Talk
Kensen ShiStanford University, Jacob SteinhardtStanford University, Percy LiangStanford University
Link to publication DOI Pre-print Media Attached File Attached
POPL-2019-Research-Papers09:44 - 10:06
Talk
Farzin HoushmandUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside
Link to publication DOI Media Attached