Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Wed 25 Oct 2017 16:59 - 17:22 at Regency A - Synthesis Chair(s): Jonathan Edwards

This paper presents natural synthesis, which generalizes the proof-theoretic synthesis technique to support very expressive logic theories. This approach leverages the natural proof methodology and reduces an intractable, unbounded-size synthesis problem to a tractable, bounded-size synthesis problem, which is amenable to be handled by modern inductive synthesis engines. The synthesized program admits a natural proof and is a provably-correct solution to the original synthesis problem. We explore the natural synthesis approach in the domain of imperative data-structure manipulations and present a novel syntax-guided synthesizer based on natural synthesis. The input to our system is a program template together with a rich functional specification that the synthesized program must meet. Our system automatically produces a program implementation along with necessary proof artifacts, namely loop invariants and ranking functions, and guarantees the total correctness with a natural proof.
Experiments show that our natural synthesizer can efficiently produce provably-correct implementations for sorted lists and binary search trees. To our knowledge, this is the first system that can automatically synthesize these programs, their functional correctness and their termination in tandem from bare-bones control flow skeletons.

Wed 25 Oct

Displayed time zone: Tijuana, Baja California change

15:30 - 17:22
SynthesisOOPSLA at Regency A
Chair(s): Jonathan Edwards
15:30
22m
Talk
Model-Assisted Machine-Code Synthesis
OOPSLA
Venkatesh Srinivasan University of Wisconsin - Madison, Ara Vartanian University of Wisconsin-Madison, USA, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
DOI
15:52
22m
Talk
Synthesis of Data Completion Scripts using Finite Tree Automata
OOPSLA
Xinyu Wang UT Austin, Isil Dillig UT Austin, Rishabh Singh Microsoft Research
DOI
16:14
22m
Talk
SQLizer: Query Synthesis from Natural Language
OOPSLA
Navid Yaghmazadeh University of Texas, Austin, Yuepeng Wang University of Texas at Austin, Isil Dillig UT Austin, Thomas Dillig
DOI
16:37
22m
Talk
Synthesizing Configuration File Specifications with Association Rule Learning
OOPSLA
Mark Santolucito Yale University, Ennan Zhai Yale University, USA, Rahul Dhodapkar MongoDB, USA, Aaron Shim Microsoft, USA, Ruzica Piskac Yale University
DOI
16:59
22m
Talk
Natural Synthesis of Provably-Correct Data-Structure Manipulations
OOPSLA
Xiaokang Qiu Purdue University, Armando Solar-Lezama MIT CSAIL
DOI