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(the step-by-step solution to a problem is like a program! PLDI 2011, IJCAI 2013b),*solution generation*(of a certain difficulty level and that exercises use of certain concepts AAAI 2014, IJCAI 2013b, CHI 2013, AAAI 2012, AAAI 2015),*problem generation*(PLDI 2013, IJCAI 2013a) , and*automated grading*(CHI 2012). Interestingly, all of these activities can be phrased as program synthesis problems.*digital content creation* **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!

*Example-based Learning in Computer-Aided STEM Education*, Conference on*Technology for Education*, Dec 2013*Program Synthesis*, Lectures at Marktoberdorf Summer School, August 2013*Synthesis for Computer-aided Education*, ExCAPE Summer School, Jun 2013*Synthesis for Intelligent Tutoring Systems*[video], ExCAPE Webinar Series, Jan 2013*End User Programming and Intelligent Tutoring Systems*, Distinguished Lecture Series at UC-Berkeley, Fall 2012*Synthesis from Examples: Interaction Models and Algorithms*, Invited Talk at SYNASC 2012*Dimensions in Synthesis*, Lectures at Summer School on Formal Methods 2012*Synthesis from Examples*, Keynote at WAMBSE 2012*Program Synthesis for Automating End-user Programming and Education*, Keynote at AVM/RiSE Meeting 2011*Usable Synthesis*, Short Invited talk at UV 2010*Dimensions in Program Synthesis*, Invited Tutorial at FMCAD 2010*Program Synthesis for Automating Education*, Keynote at AVM 2010*Dimensions in Program Synthesis*, Invited Talk at PPDP 2010*Component Based Synthesis*, Dagstuhl Seminar on Software Synthesis (December 2009)

Application |
Target User |
User Intent |
Search Technique |

Web Search Strategies [KDD 2014] | End Users | Logic | Natural Language Processing + Implicit Table Inference |

Spreadsheet Formulas [SIGMOD 2014] | End Users | Natural Language | Natural Language Processing + Type-based Synthesis |

Smartphone Scripts [MobiSys 2013] | End Users | Natural Language | Natural Language Processing + Type-based Synthesis |

Data Extraction (from text files and web pages) [PLDI 2014] | End Users | Examples | Version Space Algebra |

Data Extraction (from semi-structured spreadsheets) [PLDI 2015] | End Users | Examples | Version Space Algebra |

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 |

XML Transformations [AAAI 2014, PLDI 2014] | End Users | Examples | |

Text Transformations [UIST 2013] | End Users | Set or Sequence of Examples | |

Geometry Drawings [CHI 2012] | End Users | Sketch | |

Geometry Ruler/Compass Constructions [PLDI 2011] | Students/Teachers | Logic | |

Geometry Proof Problems [AAAI 2014] | Students/Teachers | Examples | |

Algebraic Proof Problems [AAAI 2012] | Students/Teachers | Examples | |

Procedural Math Problems [CHI 2013] | Students/Teachers | Examples | |

Natural Deduction Problems [IJCAI 2013] | Students/Teachers | Examples | |

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 |