Try Microsoft Edge A fast and secure browser that's designed for Windows 10 Get started

This site uses cookies for analytics, personalized content and ads. By continuing to browse this site, you agree to this use. Learn more

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 |