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 that support solution generation (the step-by-step solution to a problem is like a program!), problem generation (of a certain difficulty level and that exercises use of certain concepts), automated grading, and digital content creation. 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: "developing 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 from Examples [pdf], Invited Talk 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
String Transformations [POPL 2011, VLDB 2012, CACM 2012]	End-users	Examples	Version Space Algebra
Number Transformations [CAV 2012]	End-users	Examples	Version Space Algebra
Table Transformations [PLDI 2011]	End-users	Examples	Version Space Algebra
Geometry Drawings [CHI 2012]	End-users	Sketch	Deductive reasoning
Geometry Solution Generation [PLDI 2011]	Students/Teachers	Logic	Numerical Methods + A* style goal directed search
Algebra Problem Generation [AAAI 2012]	Students/Teachers	Examples	Random Testing
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
Embedded Systems [ICCPS 2010, VMCAI 2009]	System Designers	Logic + Templates	(Inductive Learning + Numerical Methods) or SMT Solvers

Research Summary Papers

Synthesis from Examples, WAMBSE 2012 (Invited Talk 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, To appear in CACM 2012, 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, 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

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, William Harris, Sumit Gulwani
[abstract |pdf |ps |Full version pdf |ppt slides]
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, Sumit Gulwani
[abstract |pdf |ppt slides |video presentation" onClick="stc(this, 67)">video presentation]
This paper describes a technology (useful for end-users) to synthesize Excel macros 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.