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:
Application | Target User | User Intent | Search Technique |
---|---|---|---|
Smartphone Scripts [MobiSys 2013] | End-users | Natural Language | Natural Language Processing + Type-based Synthesis |
Data Extraction (from text files, web pages, spreadsheets) [PLDI 2014] | 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 | Set or Sequence of Examples | Least General Generalization or Heuristic Search |
Text Transformations [UIST 2013] | End-users | Examples | Machine Learning |
Geometry Drawings [CHI 2012] | End-users | Sketch | Constraint Solving |
Geometry Ruler/Compass Constructions [PLDI 2011] | Students/Teachers | Logic | Numerical Methods + goal directed heuristic search |
Geometry Proof Problems [AAAI 2014] | Students/Teachers | Examples | Deductive Synthesis |
Algebraic Proof Problems [AAAI 2012] | Students/Teachers | Examples | Random Testing |
Procedural Math Problems [CHI 2013] | Students/Teachers | Examples | Test Case Input Generation |
Natural Deduction Problems [IJCAI 2013] | Students/Teachers | Examples | Bitvector data-structures + Offline computation |
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 |