Structuring the Synthesis of Heap-Manipulating Programs
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.
Thu 17 JanDisplayed time zone: Belfast change
09:00 - 10:06
SynthesisResearch Papers at Sala II
Chair(s): Robbert Krebbers Delft University of Technology
|Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper|
Nadia Polikarpova University of California, San Diego, Ilya Sergey Yale-NUS College and National University of SingaporeLink to publication DOI Pre-print Media Attached File Attached
|FrAngel: Component-Based Synthesis with Control Structures|
Kensen Shi Stanford University, Jacob Steinhardt Stanford University, Percy Liang Stanford UniversityLink to publication DOI Pre-print Media Attached File Attached
|Hamsaz: Replication Coordination Analysis and Synthesis|
Farzin Houshmand University of California, Riverside, Mohsen Lesani University of California, RiversideLink to publication DOI Media Attached