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:<\/p>\n
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!<\/p>\n
Application<\/strong><\/td>\n| Target User<\/strong><\/td>\n | User Intent<\/strong><\/td>\n | Search Technique<\/strong><\/td>\n<\/tr>\n | Web Search Strategies [KDD 2014<\/a>]<\/td>\n | End Users<\/td>\n | Logic<\/td>\n | Natural Language Processing + Implicit Table Inference<\/td>\n<\/tr>\n | Spreadsheet Formulas [SIGMOD 2014<\/a>]<\/td>\n | End Users<\/td>\n | Natural Language<\/td>\n | Natural Language Processing + Type-based Synthesis<\/td>\n<\/tr>\n | Smartphone Scripts [MobiSys 2013<\/a>]<\/td>\n | End Users<\/td>\n | Natural Language<\/td>\n | Natural Language Processing + Type-based Synthesis<\/td>\n<\/tr>\n | Data Extraction (from text files and web pages) [PLDI 2014<\/a>]<\/td>\n | End Users<\/td>\n | Examples<\/td>\n | Version Space Algebra<\/td>\n<\/tr>\n | Data Extraction (from semi-structured spreadsheets) [PLDI 2015<\/a>]<\/td>\n | End Users<\/td>\n | Examples<\/td>\n | Version Space Algebra<\/td>\n<\/tr>\n | String Transformations [POPL 2011<\/a>, VLDB 2012<\/a>, CACM 2012<\/a>, ICML 2013<\/a>]<\/td>\n | End Users<\/td>\n | Examples<\/td>\n | Version Space Algebra + Machine Learning<\/td>\n<\/tr>\n | Number Transformations [CAV 2012<\/a>]<\/td>\n | End Users<\/td>\n | Examples<\/td>\n | Version Space Algebra<\/td>\n<\/tr>\n | Table Transformations [PLDI 2011<\/a>]<\/td>\n | End Users<\/td>\n | Examples<\/td>\n | Version Space Algebra<\/td>\n<\/tr>\n | XML Transformations [AAAI 2014<\/a>, PLDI 2014<\/a>]<\/td>\n | End Users<\/td>\n | Examples<\/td>\n | <\/td>\n<\/tr>\n | Text Transformations [UIST 2013<\/a>]<\/td>\n | End Users<\/td>\n | Set or Sequence of Examples<\/td>\n | <\/td>\n<\/tr>\n | Geometry Drawings [CHI 2012<\/a>]<\/td>\n | End Users<\/td>\n | Sketch<\/td>\n | <\/td>\n<\/tr>\n | Geometry Ruler\/Compass Constructions [PLDI 2011<\/a>]<\/td>\n | Students\/Teachers<\/td>\n | Logic<\/td>\n | <\/td>\n<\/tr>\n | Geometry Proof Problems [AAAI 2014<\/a>]<\/td>\n | Students\/Teachers<\/td>\n | Examples<\/td>\n | <\/td>\n<\/tr>\n | Algebraic Proof Problems [AAAI 2012<\/a>]<\/td>\n | Students\/Teachers<\/td>\n | Examples<\/td>\n | <\/td>\n<\/tr>\n | Procedural Math Problems [CHI 2013<\/a>]<\/td>\n | Students\/Teachers<\/td>\n | Examples<\/td>\n | <\/td>\n<\/tr>\n | Natural Deduction Problems [IJCAI 2013<\/a>]<\/td>\n | Students\/Teachers<\/td>\n | Examples<\/td>\n | <\/td>\n<\/tr>\n | Grading of Introductory Programming Assignments [PLDI 2013<\/a>]<\/td>\n | Students\/Teachers<\/td>\n | Sample Solution<\/td>\n | Edit-distance based search using Sketch<\/td>\n<\/tr>\n | Grading of Automata Constructions [IJCAI 2013<\/a>]<\/td>\n | Students\/Teachers<\/td>\n | Sample Solution<\/td>\n | Edit-distance based Search<\/td>\n<\/tr>\n | Recursive Programs [CAV 2013<\/a>]<\/td>\n | End Users<\/td>\n | Examples<\/td>\n | Goal-directed Search<\/td>\n<\/tr>\n | Biological Synthesis<\/span> [Distraction 2013<\/a>]<\/td>\n | First-time PL parents<\/td>\n | (lack of) Logic<\/td>\n | Template-based and Inductive<\/td>\n<\/tr>\n | Vectorized Code [PPoPP 2013<\/a>]<\/td>\n | Software developers<\/td>\n | Loop to be vectorized<\/td>\n | Combination of Deductive and Inductive Synthesis<\/td>\n<\/tr>\n | API Discovery and Code Completion [PLDI 2012<\/a>]<\/td>\n | Software developers<\/td>\n | Partial Expression<\/td>\n | Type-based search and ranking<\/td>\n<\/tr>\n | Program Inverses [PLDI 2011<\/a>]<\/td>\n | Software developers<\/td>\n | Templates<\/td>\n | PathTesting-based synthesis + SMT solvers<\/td>\n<\/tr>\n | Bit-vector Algorithms [PLDI 2011<\/a>, ICSE 2010<\/a>]<\/td>\n | Algorithm designers<\/td>\n | (Logic or Examples) + Components<\/td>\n | SMT solvers<\/td>\n<\/tr>\n | Graph Algorithms [OOPSLA 2010<\/a>]<\/td>\n | Algorithm designers<\/td>\n | Logic<\/td>\n | Inductive Learning + SAT solvers<\/td>\n<\/tr>\n | Undergraduate Textbook Algorithms [POPL 2010<\/a>]<\/td>\n | Algorithm designers<\/td>\n | Logic + Templates<\/td>\n | Invariant-based synthesis + SMT solvers<\/td>\n<\/tr>\n | Switching Logic [ICCPS 2010<\/a>, VMCAI 2009<\/a>]<\/td>\n | Embedded-system designers<\/td>\n | Logic + Templates<\/td>\n | (Inductive Learning + Numerical Methods) or SMT Solvers<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n | <\/p>\n","protected":false},"excerpt":{"rendered":" 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: (100s of millions of) End Users (people who have access […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-361034","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2010-01-01","related-publications":[164710,336380,335258,335696,166504,336386,335279,335714,168017,336518,335291,335804,238207,335327,335825,238222,335339,335843,238223,335348,335864,238224,335447,335900,268593,335471,159375,335936,317504,335492,160306,336008,326828,335543,162576,336026,334466,335552],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","value":"sumitg","display_name":"Sumit Gulwani","author_link":"Sumit Gulwani<\/a>","is_active":false,"user_id":33755,"last_first":"Gulwani, Sumit","people_section":0,"alias":"sumitg"}],"msr_research_lab":[],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/361034"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":4,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/361034\/revisions"}],"predecessor-version":[{"id":390179,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/361034\/revisions\/390179"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=361034"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=361034"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=361034"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=361034"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=361034"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}} |