Program Synthesis


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:

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

Dimensions in Program Synthesis [PPDP 2010]

Application Target User User Intent Search Technique
Web Search Strategies [KDD 2014]End UsersLogicNatural Language Processing + Implicit Table Inference
Spreadsheet Formulas [SIGMOD 2014]End UsersNatural LanguageNatural Language Processing + Type-based Synthesis
Smartphone Scripts [MobiSys 2013]End UsersNatural LanguageNatural Language Processing + Type-based Synthesis
Data Extraction (from text files and web pages) [PLDI 2014]End UsersExamplesVersion Space Algebra
Data Extraction (from semi-structured spreadsheets) [PLDI 2015]End UsersExamplesVersion Space Algebra
String Transformations [POPL 2011, VLDB 2012, CACM 2012, ICML 2013]End UsersExamplesVersion Space Algebra + Machine Learning
Number Transformations [CAV 2012]End UsersExamplesVersion Space Algebra
Table Transformations [PLDI 2011]End UsersExamplesVersion Space Algebra
XML Transformations [AAAI 2014, PLDI 2014]End UsersSet or Sequence of ExamplesLeast General Generalization or Heuristic Search
Text Transformations [UIST 2013]End UsersExamplesMachine Learning
Geometry Drawings [CHI 2012]End UsersSketchConstraint Solving
Geometry Ruler/Compass Constructions [PLDI 2011]Students/TeachersLogicNumerical Methods + goal directed heuristic search
Geometry Proof Problems [AAAI 2014]Students/TeachersExamplesDeductive Synthesis
Algebraic Proof Problems [AAAI 2012]Students/TeachersExamplesRandom Testing
Procedural Math Problems [CHI 2013]Students/TeachersExamplesTest Case Input Generation
Natural Deduction Problems [IJCAI 2013]Students/TeachersExamplesBitvector data-structures + Offline computation
Grading of Introductory Programming Assignments [PLDI 2013]Students/TeachersSample SolutionEdit-distance based search using Sketch
Grading of Automata Constructions [IJCAI 2013]Students/TeachersSample SolutionEdit-distance based Search
Recursive Programs [CAV 2013]End UsersExamplesGoal-directed Search
Biological Synthesis [Distraction 2013]First-time PL parents(lack of) LogicTemplate-based and Inductive
Vectorized Code [PPoPP 2013]Software developersLoop to be vectorizedCombination of Deductive and Inductive Synthesis
API Discovery and Code Completion [PLDI 2012]Software developersPartial ExpressionType-based search and ranking
Program Inverses [PLDI 2011]Software developersTemplatesPathTesting-based synthesis + SMT solvers
Bit-vector Algorithms [PLDI 2011, ICSE 2010]Algorithm designers(Logic or Examples) + ComponentsSMT solvers
Graph Algorithms [OOPSLA 2010]Algorithm designersLogicInductive Learning + SAT solvers
Undergraduate Textbook Algorithms [POPL 2010]Algorithm designersLogic + TemplatesInvariant-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

Regular Papers