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:

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

Dimensions in Program Synthesis [PPDP 2010]

Application Target User User Intent Search Technique
String Transformations [POPL 2011, VLDB 2012, CACM 2012]End-usersExamplesVersion Space Algebra
Number Transformations [CAV 2012]End-usersExamplesVersion Space Algebra
Table Transformations [PLDI 2011]End-usersExamplesVersion Space Algebra
Geometry Drawings [CHI 2012]End-usersSketchDeductive reasoning
Geometry Solution Generation [PLDI 2011]Students/TeachersLogicNumerical Methods + A* style goal directed search
Algebra Problem Generation [AAAI 2012]Students/TeachersExamplesRandom Testing
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
Embedded Systems [ICCPS 2010, VMCAI 2009]System Designers Logic + Templates(Inductive Learning + Numerical Methods) or SMT Solvers

Research Summary Papers

Regular Papers