Program Synthesis

Introduction

Program synthesis is the task of automatically discovering an executable piece of code given user intent expressed using various forms of constraints such as input-output examples, demonstrations, natural language, etc. Program synthesis has direct applications for various classes of users in the technology pyramid:

(100s of millions of) End-users (people who have access to a computational device but are not expert programmers): Helping them to create small snippets of code for performing repetitive tasks, simple data manipulation. In other words, enabling them to bring their creativity to life!
(Billions of) Students and Teachers: Intelligent tutoring systems (pdf, video) that support solution generation (the step-by-step solution to a problem is like a program! PLDI 2011, IJCAI 2013b), problem generation (of a certain difficulty level and that exercises use of certain concepts IJCAI 2013b, CHI 2013, AAAI 2012), automated grading (PLDI 2013, IJCAI 2013a) , and digital content creation (CHI 2012). Interestingly, all of these activities can be phrased as program synthesis problems.
Software Developers: Help synthesize mundane pieces of code.
Algorithm Designers: Help discover new algorithms

Recent advances in AI-style search techniques and formal reasoning techniques based on SAT/SMT solvers have made it possible to efficiently synthesize small programs. I strongly believe that the program synthesis technology is now set to create the next revolution in computing. And hence I spend most of my time working in this area: "devHIeloping new program synthesis techniques and incorporating them into easy-to-use tools" with the goal of democratizing effective use of computational devices, thereby enabling people to bring their creativity to life!

Selected Invited Talks

Synthesis for Intelligent Tutoring Systems [ppt |video], ExCAPE Webinar Series, Jan 2013
End User Programming and Intelligent Tutoring Systems [ppt], Distinguished Lecture Series at UC-Berkeley, Fall 2012
Synthesis from Examples: Interaction Models and Algorithms [ppt], Invited Talk at SYNASC 2012
Dimensions in Synthesis [Lecture 1(ppt, pdf)], [Lecture 2(ppt, pdf)], [Lecture 3(ppt, pdf)], Lectures at Summer School on Formal Methods 2012
Synthesis from Examples [pdf], Keynote at WAMBSE 2012
Program Synthesis for Automating End-user Programming and Education, Keynote at AVM/RiSE Meeting 2011
Usable Synthesis [ppt], Short Invited talk at UV 2010
Dimensions in Program Synthesis [ppt], Invited Tutorial at FMCAD 2010
Program Synthesis for Automating Education [ppt], Keynote at AVM 2010
Dimensions in Program Synthesis [ppt], Invited Talk at PPDP 2010
Component Based Synthesis [ppt], Dagstuhl Seminar on Software Synthesis

Dimensions in Program Synthesis [PPDP 2010]

Application	Target User	User Intent	Search Technique
Smartphone Scripts [MobiSys 2013]	End-users	Natural Language	Natural Language Processing + Type-based Synthesis
String Transformations [POPL 2011, VLDB 2012, CACM 2012, ICML 2013]	End-users	Examples	Version Space Algebra + Machine Learning
Number Transformations [CAV 2012]	End-users	Examples	Version Space Algebra
Table Transformations [PLDI 2011]	End-users	Examples	Version Space Algebra
Text Transformations [UIST 2013]	End-users	Examples	Machine Learning
Geometry Drawings [CHI 2012]	End-users	Sketch	Constraint Solving
Geometry Ruler/Compass Constructions [PLDI 2011]	Students/Teachers	Logic	Numerical Methods + A* style goal directed search
Algebraic Proof Problems [AAAI 2012]	Students/Teachers	Examples	Random Testing
Procedural Math Problems [CHI 2013]	Students/Teachers	Examples	Test Case Input Generation
Natural Deduction Problems [IJCAI 2013]	Students/Teachers	Examples	Bitvector data-structures + Offline computation
Grading of Introductory Programming Assignments [PLDI 2013]	Students/Teachers	Sample Solution	Edit-distance based search using Sketch
Grading of Automata Constructions [IJCAI 2013]	Students/Teachers	Sample Solution	Edit-distance based Search
Recursive Programs [CAV 2013]	End-users	Examples	Goal-directed Search
Biological Synthesis [Distraction 2013]	First-time PL parents	(lack of) Logic	Template-based and Inductive
Vectorized Code [PPoPP 2013]	Software developers	Loop to be vectorized	Combination of Deductive and Inductive Synthesis
API Discovery and Code Completion [PLDI 2012]	Software developers	Partial Expression	Type-based search and ranking
Program Inverses [PLDI 2011]	Software developers	Templates	PathTesting-based synthesis + SMT solvers
Bit-vector Algorithms [PLDI 2011, ICSE 2010]	Algorithm designers	(Logic or Examples) + Components	SMT solvers
Graph Algorithms [OOPSLA 2010]	Algorithm designers	Logic	Inductive Learning + SAT solvers
Undergraduate Textbook Algorithms [POPL 2010]	Algorithm designers	Logic + Templates	Invariant-based synthesis + SMT solvers
Switching Logic [ICCPS 2010, VMCAI 2009]	Embedded-system designers	Logic + Templates	(Inductive Learning + Numerical Methods) or SMT Solvers

Research Summary Papers

Formal Methods for Computer-Aided STEM Education, MSR Technical Report 2013, Sumit Gulwani
[abstract |pdf |bibtex]

Synthesis from Examples: Interaction Models and Algorithms, SYNASC 2012, Keynote Paper, Sumit Gulwani
[abstract |pdf |bibtex]
This invited talk paper presents describes various user interaction models and algorithms for inductive synthesis. It also describes some useful and surprising applications from domains of end-user programming and intelligent tutoring systems.

Synthesis from Examples, WAMBSE 2012, Keynote Paper, Sumit Gulwani
[abstract |pdf |bibtex]
This invited talk paper presents varied applications for synthesis-by-example technology (mostly from the areas of end-user programming and intelligent tutoring systems).

Spreadsheet Data Manipulation using Examples, CACM 2012, Research Highlights Paper, Sumit Gulwani, William Harris, Rishabh Singh
[abstract |pdf]
This CACM research highlights paper presents three different inductive synthesizers based on version-space algebras using a common formalism.

Dimensions in Program Synthesis, PPDP 2010, Keynote Paper, Sumit Gulwani
[abstract |pdf |ppt]
This invited talk paper presents a survey of various applications and state-of-the-art techniques for program synthesis. It is based around description of three dimensions in program synthesis: (a) expression of user intent, (b) search space of programs, and (c) search technique.

Template-based Program Verification and Program Synthesis, Journal on Software Tools for Technology Transfer, Saurabh Srivastava, Sumit Gulwani, Jeff Foster
[abstract |pdf] (Final version available at Springerlink)
This journal paper summarizes several years of our work on template based program verification and describes how it laid the foundation for our follow-up work on template-based program synthesis.

Regular Papers

SmartSynth: Synthesizing Smartphone Automation Scripts from Natural Language, To appear in MobiSys 2013, Vu Le, Sumit Gulwani, Zhendong Su
[abstract]
This paper innovates in two ways: First, it applies program synthesis to a new domain of smartphone programming. Second, it shows how to synthesize scripts from natural language descriptions.

Automatically Generating Problems and Solutions for Natural Deduction, To appear in IJCAI 2013, Umair Ahmed, Sumit Gulwani, Amey Karkare
[abstract |pdf]
This paper proposes use of bitvector data-structures (thereby avoiding symbolic reasoning) and use of offline computation to speed up search for both solutions and problems.

Automated Grading of DFA constructions, To appear in IJCAI 2013, Rajeev Alur, Loris D'Antoni, Sumit Gulwani, Dileep Kini, Mahesh Viswanathan
[abstract |pdf |full-version(pdf)]
This paper proposes basing grading on some interesting metrics namely density of counterexamples, edit-distance to a correct solution, and edit-distance between the correct problem description and a problem description synthesized from the student's solution.

Automated Feedback Generation for Introductory Programming Assignments, To appear in PLDI 2013, Rishabh Singh, Sumit Gulwani, Armando Solar-Lezama
[abstract]
This paper proposes basing feedback on edit-distance to a correct solution, and the search for that correct solution is phrased as a sketching based program synthesis problem.

A Colorful Approach to Text Processing by Example, To appear in UIST 2013, Kuat Yessenov, Shubham Tulsiani, Aditya Menon, Rob Miller, Sumit Gulwani, Butler Lampson, Adam Kalai
[abstract]
This paper innovates by introducing notions of (mock) examples for discovering structure in a text document to enable sophisticated text transformations.

A Trace-based Framework for Analyzing and Synthesizing Educational Progressions, To appear in CHI 2013, Erik Andersen, Sumit Gulwani, Zoran Popovic
[abstract |pdf]
This paper shows how to generate practice problems for procedural content in middle-school mathematics using test case input generation techniques.

Recursive Program Synthesis, To appear in CAV 2013, Aws Albarghouthi, Sumit Gulwani, Zachary Kincaid
[abstract]
This paper presents a new technique for synthesizing recursive programs from examples.

A Machine Learning Framework for Programming by Example, To appear in ICML 2013, Aditya Menon, Omer Tamuz, Sumit Gulwani, Butler Lampson, Adam Kalai
[abstract |pdf]
This paper shows how to improve efficiency of brute-force search as well as ranking by prioritizing certain program operators over others based on textual cues from examples.

From Relational Verification to SIMD Loop Synthesis, PPoPP 2013, Best Paper Award , Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, Cesar Kunz, Mark Marron
[abstract |pdf]
This paper describes a synthesis methodology for automatically generating vectorized code fragments.

Automatically Generating Algebra Problems, AAAI 2012, Rohit Singh, Sumit Gulwani, Sriram Rajamani
[abstract |pdf |full-version(pdf)]
This paper describes a by-example technology for generating new algebra problems that have the same difficult level as that of a given algebra problem.

Synthesizing Number Transformations from Input-Output Examples, CAV 2012, Rishabh Singh, Sumit Gulwani
[abstract |pdf |full-version(pdf)]

Learning Semantic String Transformations from Examples, VLDB 2012, Rishabh Singh, Sumit Gulwani
[abstract |pdf]

Type-Directed Completion of Partial Expressions, PLDI 2012, Daniel Perelman, Sumit Gulwani, Tom Ball, Dan Grossman
[abstract |pdf (draft version)]

QuickDraw: Improving Drawing Experience for Geometric Diagrams, CHI 2012, Salman Cheema, Sumit Gulwani, Joseph LaViola
[abstract |pdf]

Synthesizing Geometry Constructions, PLDI 2011, Sumit Gulwani, Vijay Korthikanti, Ashish Tiwari
[abstract |pdf |ps |ppt slides]
This paper describes a technique (useful for students/teachers) to synthesize ruler/compass based geometry constructions from logical problem descriptions.

Synthesis of Loop-Free Programs, PLDI 2011, Sumit Gulwani, Susmit Jha, Ashish Tiwari, Ramarathnam Venkatesan
[abstract |pdf |ps |ppt slides]
This paper describes a technique (useful for designers) to assemble a given multi-set of components in a loop-free manner, given the logical functional specification for each component and for the desired assembly.

Spreadsheet Table Transformations from Examples, PLDI 2011, Invited to CACM Research Highlights [citation], William Harris, Sumit Gulwani
[abstract |pdf |ps |Full version pdf |ppt slides |CACM version(pdf)]
This paper describes a technique (useful for end-users) to synthesize scripts for transforming spreadsheet tables, given examples of such transformations.

Path-based Inductive Synthesis for Program Inversion, PLDI 2011, Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, Jeff Foster
[abstract |pdf |ps |pdf slides]
This paper describes a technique (useful for programmers) to synthesize inverses of given programs. The technique is a more general synthesis technique that achieves a good trade-off between efficiency and correctness by combining ideas from testing and verification.

Automating String Processing in Spreadsheets using Input-Output Examples, POPL 2011, Invited to CACM Research Highlights [citation], Sumit Gulwani
[abstract |pdf |ppt slides |video presentation |CACM version(pdf) |Shipped as Flash Fill feature in Excel 2013]
This paper describes a technology (useful for end-users) to synthesize string transformations from input-output examples.

Oracle-Guided Component-Based Program Synthesis, ICSE 2010, Susmit Jha, Sumit Gulwani, Sanjit Seshia and Ashish Tiwari
[abstract |ps |pdf]

This paper introduces an active learning technique that is applied to synthesis of bit-vector algorithms from input-output examples. Bit-vector algorithms, as referred to in this paper, are small straight-line pieces of code that are tricky to get right since they involve unintuitive combination of arithmetic and logical operators.

From Program Verification to Program Synthesis, POPL 2010, Saurabh Srivastava and Sumit Gulwani and Jeff Foster
[abstract |ps |pdf |ppt slides]

This paper shows how to leverage formal reasoning techniques based on SMT solvers (traditionally used for program verification) for program synthesis.

A Simple Inductive Synthesis Methodology and its Applications, OOPSLA 2010, Shachar Itzhaky, Sumit Gulwani, Neil Immerman, and Mooly Sagiv
[abstract |pdf]
This paper shows how to synthesize efficient graph algorithms (such as checking whether a graph is bipartite or not) from natural but inefficient higher-order logic specifications.

Synthesizing Switching Logic for Safety and Dwell-Time Requirement, ICCPS 2010, Susmit Jha, Sumit Gulwani, Sanjit Seshia and Ashish Tiwari
[abstract| pdf| full-version(pdf)]
This paper shows how to combine various interesting technologies to enable synthesis of switching logic in hybrid systems.

Synthesizing Switching Logic using Constraint Solving, VMCAI 2009, Ankur Taly, Sumit Gulwani, and Ashish Tiwari
[abstract |ps |pdf |pdf slides]
This paper shows an application of constraint solving technology to synthesis of switching logic in hybrid systems.