About

Sumit Gulwani is a Research manager at Microsoft, leading the PROSE research and engineering team that develops APIs for program synthesis (programming by examples and natural language) and incorporates them into real products. His programming-by-example work led to the Flash Fill feature of Microsoft Excel 2013 that is used by hundreds of millions of people. Sumit has published 110+ papers in top-tier conferences/journals across multiple computer science areas, and delivered 30+ keynotes/invited talks at various forums. He was awarded the ACM SIGPLAN Robin Milner Young Researcher Award in 2014 for his pioneering contributions to end-user programming and intelligent tutoring systems. He obtained his PhD in Computer Science from UC-Berkeley in 2005, and was awarded the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in Computer Science and Engineering from IIT Kanpur in 2000, and was awarded the President’s Gold Medal.

Projects

Logan: Logfile Analysis

Established: October 12, 2015

Understanding Techniques and Tools for More Effective Telemetry and Log Data Analysis. Increasingly, business processes require data-driven real-time feedback based on large quantities of log data and customer telemetry from multiple sources. The Logan Project takes a broad approach to understanding the specific needs of consumers of telemetry and log data, focusing on giving them better support for extracting the data they need, cleaning it, and creating queries against it. To understand…

Automated Problem Generation for Education

Established: February 25, 2013

Intelligent Tutoring Systems (ITS) can significantly enhance the educational experience, both in the classroom and online. A key aspect of ITS is the ability to automatically generate problems of a certain difficulty level and that exercise use of certain concepts. This can help avoid copyright or plagiarism issues and help generate personalized workflows. This project develops technologies for problem generation in various subject domains including math, logic, and even language learning. Team This is an…

FlashExtract

Established: January 1, 2013

(Programming-by-example APIs for extracting structured data from text/log files by examples) The FlashExtract technology (published as a PLDI 2014 paper [pdf |ppt slides |Video |Video 2]) ships as features in Powershell and Azure OMS (Operations Management Suite). FlashExtract powers the ConvertFrom-String cmdlet in Powershell. Here's a Microsoft blogpost that explains this cmdlet. Here are some videos prepared by others to demonstrate this capability: Example-driven parsing Doug Finke's UI Here are some blogposts Powershell PowerShell 5.0…

Flash Fill (Excel feature in Office 2013)

Established: January 1, 2012

Our programming by example work (POPL 2011), also recognized as CACM Research Highlights (CACM 2012), ships as part of the Flash Fill feature in Excel in Office 2013. Here's a small video illustrating this feature. Here's another small video illustrating potential extensions. Here's the inside story of how it came about: Flash Fill Gives Excel a Smart Charge Here are some other videos on FlashFill You-tube: Excel 2013 Flash Fill: 23 Amazing Examples, Excel 2013-…

Program Synthesis

Established: January 1, 2010

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 to a computational device but are not expert programmers): Helping them to create small snippets of code for performing repetitive…

VS3 (Verification and Specification using SMT Solvers)

Established: December 1, 2009

SMT Solvers have traditionally been used for verifying correctness of systems that have been annotated with relevant inductive invariants. Such an annotation usually is an undesirable burden on the user. This project explores techniques for using SMT solvers to automatically discover inductive invariants for proving given safety properties of systems. Additionally, this project also explores techniques for using SMT solvers to synthesize systems in the first place given enough specifications. Saurabh Srivastava, who is leading…

SPEED (Symbolic Resource Time/Space Bounds Analysis)

Established: December 1, 2008

Introduction Performance measurement of software is a critical component of software development. Performance is traditionally measured using profiling, which is often too little (only certain inputs are profiled) or too late (to make requisite changes to address the root cause before shipping). The SPEED project attempts to address these limitations by static estimation of symbolic computational complexity of programs. It builds over recent advances in static program analysis, which has traditionally been used for checking…

Random Interpretation (Random Testing + Abstract Interpretation)

Established: December 1, 2008

Randomized Algorithms for Formal Verification Powerpoint Slides on Random Interpretation Introduction A sound and complete program analysis is provably hard. We typically pay a price for the hardness of program analysis in terms of having an incomplete (i.e. conservative) analysis, or by having algorithms that are complicated and have long running-time. It is interesting to consider if we can pay for this hardness by compromising soundness a little bit (and thus benefit by having simpler…

Logical Abstract Interpretation

Established: November 3, 2008

Abstract Interpretation over Logical Formulas Powerpoint Slides on Logical Abstract Interpretation (Lectures given in a graduate class on Static Program Analysis at UCLA and at IISc-Bangalore) Introduction Logical Abstract Interpretation means performing abstract interpretation over abstract domains whose elements are logical formulas over some theory and the partial order relationship is the implication relationship (or some refinement of it). Theorem proving community has studied decision procedures for several theories. For performing abstract interpretation over logical formulas…

Publications

2017

2016

2015

Automating Grammar Comparison
Ravichandhran Madhavan, Mikaël Mayer, Sumit Gulwani, Viktor Kuncak, in OOPSLA 2015 Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 25, 2015, View abstract, Download PDF

2014

2013

2012

2011

2010

2009

2008

Ranking Abstractions
Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang, in Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science., Springer, Berlin, Heidelberg, January 1, 2008, View abstract, Download PDF

2007

2006

2005

2004

2003

2000

Projects

Link description

Computer-Aided Education

Date

July 15, 2013

Speakers

Armando Solar-Lezama, Sumit Gulwani, and Zoran Popovic

Affiliation

Massachusetts Institute of Technology, MSR, University of Washington

Other

Biography

I currently lead a research & engineering group at Microsoft that develops programming-by-example technologies for data wrangling. These technologies power various features in several Microsoft products. If you are excited about doing research in the cross-disciplinary area of program synthesis, productizing that research, and be part of a team of incredible researchers and engineers, please ping me.

I am also interested in building intelligent tutoring systems (which support activities such as automated problem generation and feedback generation) for various K-14 subject domains including math, programming, and language learning. I mentor several undergraduate and graduate students. If you are looking for disruptive project ideas related to intelligent tutoring systems or automating end-user programming (and are excited about the potential to positively impacting lives of billions of people on the planet!), please send me email.

I obtained my Phd in Computer Science from UC-Berkeley in 2005, and my undergraduate degree in Computer Science and Engineering from IIT Kanpur in 2000.

Research Highlights

Distraction: Invited Talk on Biological Synthesis (ppt) given at RiSE research group meeting. A recommended read for PL researchers wanting to be first-time parents.

Media/Blog posts

Phd Students (co-advised by me)

Resume

Download my resume here.

Primary Affiliation: Principal Researcher @ Microsoft Research, Redmond lab [since August 2005]

Other Affiliations: Adjunct Faculty @ IIT Kanpur [since Fall 2012]

Affiliate Faculty @ University of Washington [since Fall 2012]

Address: Microsoft Corporation, One Microsoft Way, Redmond, WA, 98052 | Email: sumitg@microsoft.com | Phone: (+1) 425-706-7709 | Homepage: https://www.microsoft.com/en-us/research/people/sumitg/

Employment and Education

  • Principal Researcher (March 2014 – present) Microsoft Research, Redmond, USA
  • Senior Researcher (June 2011 – Feb 2014) Microsoft Research, Redmond, USA
  • Researcher (August 2005 – May 2011) Microsoft Research, Redmond, USA
  • Ph.D., Computer Science (2000-2005) University of California at Berkeley Advisor: Prof. George Necula
  • B.Tech, Computer Science and Engineering (1996-2000) Indian Institute of Technology (IIT), Kanpur, India GPA: 4.00

Awards

  • Distinguished Artifact Award, PLDI 2015
  • ACM SIGPLAN Robin Milner Young Researcher Award, 2014 [citation]
  • Distinguished Paper Award, PLDI 2013
  • Best Paper Award, PPoPP 2013
  • MSR Outstanding Contributions to Impossible Things Initiative, 2012 (for Program Synthesis work)
  • Distinguished Paper Award, FSE 2011
  • Microsoft Thought Leadership Award, 2011 (for Office-by-Example technology).
  • Microsoft Gold Star Award, 2010.
    • Citation: “For exceptional contributions, in particular technical vision and leadership, strong collaborative efforts, and development of key synthesis technologies.”
  • Microsoft Golden Volcano Award and runner-up for Thought Leadership Award, 2010 (for Excel-by-Example technology).
  • Microsoft Gold Star Award, 2008.
    • Citation: “For unusual maturity in pursuing a challenging and coherent research agenda (new foundational program analysis techniques) and applying it to unconventional program analysis problems with strong results.”
  • IIT Kanpur West Coast Alumni Leadership Award, 2008.
    • Citation: “For recognition of his leadership as a young alumni and for contributions to research excellence”
  • ACM SIGPLAN Outstanding Doctoral Dissertation Award, 2005.
  • C.V. Ramamoorthy Distinguished Research Award for outstanding contributions to a new research area in computer science, 2005.
  • Microsoft Research Fellowship for graduate studies, 2004-05.
  • UC Regents Fellowship for graduate studies, 2000-01.
  • President’s Gold Medal award for best academic performance in the graduating class in all disciplines of the undergraduate programmes at IIT Kanpur, May 2000.
  • Proficiency award for best project (final year thesis) in Computer Science and Engineering discipline at IIT Kanpur, May 2000.
  • Dr. V. Rajaraman Scholarship for excellent academic performance at IIT Kanpur, 1999-00.
  • Hughes Software Systems Best Student award (at national level), 1998.
  • Qualified for Singapore Airlines Fellowship (SIA-NOL Scholarship) for undergraduate studies in Nanyang Technological University, Singapore (1995).
  • City Montessori School Best Student award (among more than 1000 students), 1995.
  • National Talent Search Scholarship awarded by the government of India, 1993-2000.

Professional Activities and Accomplishments

Invited Lectures (1 week each)

  • Programming by Examples, In Marktoberdorf International Summer School, 2015
  • Program Synthesis, In Marktoberdorf International Summer School, August 2013
  • Dimensions in Program Synthesis, In Summer School on Formal Techniques at Menlo College, Atherton, CA, May 2012
  • Art of Invariant Generation applied to Symbolic Bound Computation, In Summer School on Logic and Theorem Proving in Programming Languages at University of Oregon, 2009
  • Logical Abstract Interpretation, In Graduate Course on Static Program Analysis at UCLA, May 2008
  • Logical Abstract Interpretation, In Graduate Course on Program Analysis and Verification at IISc-Bangalore, 2007

Keynotes/Invited Talks

  • Spreadsheet Programming using Examples, SEMS 2016
  • Programming by Examples, IJCAR 2016
  • Applications of Formal Methods to Data Wrangling and Education, Brazilian Symposium on Formal Methods 2015
  • Programming by Examples applied to Data Wrangling, SYNT 2015
  • Data Wrangling using Programming by Examples, ECOOP 2015
  • Data Manipulation using Programming By Examples and Natural Language, Distinguished Lecture Series at UPenn (April 2015)
  • Automating Repetitive Tasks for the Masses, Keynote at POPL 2015
  • Cultivating Research Taste (illustrated via a journey in program synthesis research), Invited Talk at PLMW 2015
  • Applications of Program Synthesis to End-User Programming and Intelligent Tutoring Systems, Invited Talk at ILP 2014
  • Problem Generation and Feedback Generation, Invited Talk at ASSESS 2014
  • Applications of Program Synthesis to End-User Programming and Intelligent Tutoring Systems, Keynote at GECCO 2014, Genetic Programming Track
  • Example-based learning in computer-aided STEM Education, Keynote at IEEE Conference on Technology for Education (T4E), Dec 2013
  • End-User Programming and Intelligent Tutoring Systems, Invited Talk at Maryland CS Colloquium, Sep 2013
  • Synthesis for Computer-aided Education, Invited Talk at ExCAPE Summer School on Software Synthesis, June 2013
  • Synthesis from Examples: Interaction Models and Algorithms, Invited Talk at SYNASC 2012
  • End User Programming and Intelligent Tutoring Systems, Distinguished Lecture Series at UC-Berkeley, Fall 2012.
  • Synthesis from Examples, Keynote at WAMBSE 2012
  • Continuity and Robustness of Programs, Invited Talk at ISEC 2012
  • Program Synthesis for Automating End-user Programming and Education, Keynote at PASTE 2011
  • Program Synthesis for Automating End-user Programming and Education, Keynote at AVM/RiSE Meeting 2011
  • 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
  • The Fixpoint Brush in the Art of Invariant Generation, Invited Talk at WING 2010
  • Component Based Synthesis, Dagstuhl Seminar on Software Synthesis (December 2009)
  • The Reachability-Bound Problem, Invited Talk at FOPARA 2009
  • The Art of Invariant Generation for Symbolic Loop Bound Analysis, Invited Talk at CAV 2009
  • Symbolic Complexity Bounds Analysis, Computer Science Colloquium at Cornell, October 2008.
  • Symbolic Complexity Bounds Analysis, Invited Talk at HAV 2008
  • Program Verification using Probabilistic Techniques, Keynote at Workshop on Verified Software: Tools, Techniques, and Experiments, Floc 2006
  • Random Interpretation. Job-interview talk given at computer science departments of several graduate schools: CMU, Cornell, Caltech, UIUC, UPenn, UW-Madison, UMich-Ann Arbor, UC-San Diego, UMass-Amherst, Purdue, and NYU, Feb-May 2005.

Refereed Conference and Journal Publications

  • [Marktoberdorf Lecture Notes]Programming by Examples (and its applications in data wrangling)
  • [CACM ’16] Program Synthesis using Stochastic Techniques
  • [ICSE ’16] Program Synthesis using Natural Language
  • [POPL ’16] Transforming Spreadsheet Data Types using Examples
  • [CACM ’15] Inductive Programming Meets the Real World
  • [OOPSLA ’15] FlashMeta: A Framework for Inductive Program Synthesis
  • [OOPSLA ’15] Automating Grammar Comparison
  • [UIST ’15] User Interaction Models for Disambiguation in Programming by Example
  • [CAV ’15] Predicting a Correct Program in Programming By Example
  • [IJCAI ’15] FlashNormalize: Programming by Examples for Text Normalization
  • [IJCAI ’15] Compositional Program Synthesis from Natural Language and Examples
  • [IJCAI ’15] Personalized Mathematical Word Problem Generation
  • [PLDI ’15] FlashRelate: Extracting Relational Data from Semi-Structured Spreadsheets Using Examples
  • [ICSE ’15 Demonstrations Track] StriSynth: Synthesis for Live Programming
  • [TOCHI ’15] How Can Automatic Feedback Help Students Construct Automata?
  • [CHI ’15] A Framework for Automatically Generating Interactive Tutorials
  • [CHI ’15] Automatic Game Progression Design through Analysis of Solution Features
  • [CHI ’15] Mixed-Initiative Approaches to Global Editing in Slideware
  • [AAAI ’15] Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games
  • [POPL ’15] Automating Repetitive Tasks for the Masses (Keynote Paper)
  • [CACM ’14] Example-Based Learning in Computer-Aided STEM Education
  • [FSE ’14] Feedback Generation for Performance Problems in Introductory Programming Assignments
  • [KDD ’14] LaSEWeb: Automating Search Strategies Over Semi-structured Web Data
  • [GECCO ’14] Applications of Program Synthesis to End-User Programming and Intelligent Tutoring Systems (Invited Talk Paper)
  • [SIGMOD ’14] NLyze: Interactive Programming by Natural Language for SpreadSheet Data Analysis and Manipulation
  • [AAAI ’14] Programming by Example using Least General Generalizations
  • [AAAI ’14] Automatic Synthesis of Geometry Problems for an Intelligent Tutoring System
  • [PLDI ’14] FlashExtract: A Framework for Data Extraction by Examples
  • [PLDI ’14] Test-Driven Synthesis
  • [IUI ’14] A Practical Framework for Constructing Structured Drawings
  • [LPAR ’13] Solving Geometry Problems using a Combination of Symbolic and Numerical Reasoning
  • [UIST ’13] A Colorful Approach to Text Processing by Example
  • [MobiSys ’13] SmartSynth: Synthesizing Smartphone Automation Scripts from Natural Language
  • [IJCAI ’13] Automatically Generating Problems and Solutions for Natural Deduction
  • [IJCAI ’13] Automated Grading of DFA constructions
  • [CAV ’13] Recursive Program Synthesis
  • [PLDI ’13] Automated Feedback Generation for Introductory Programming Assignments
  • [PLDI ’13] Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths
  • [CHI ’13] A Trace-based Framework for Analyzing and Synthesizing Educational Progressions
  • [ICML ’13] A Machine Learning Framework for Programming by Example
  • [PPoPP ’13] From Relational Verification to SIMD Loop Synthesis (Best Paper Award & Nominated for CACM Research Highlights)
  • [SYNASC ’12] Synthesis from Examples: Interaction Models and Algorithms (Keynote Paper)
  • [CACM ’12] Spreadsheet Data Manipulation using Examples (CACM Research Highlights)
  • [CACM ’12] Continuity and Robustness of Programs (CACM Research Highlights)
  • [WAMBSE ’12] Synthesis from Examples (Keynote Paper)
  • [AAAI ’12] Automatically Generating Algebra Problems
  • [VLDB ’12] Learning Semantic String Transformations from Examples
  • [PLDI ’12] Type-Directed Completion of Partial Expressions
  • [CHI ’12] QuickDraw: Improving Drawing Experience for Geometric Diagrams
  • [CAV ’12] Synthesizing Number Transformations from Input-Output Examples
  • [JSTTT ’12] Template-based Program Verification and Program Synthesis (Journal paper)
  • [FSE ’11] Proving Programs Robust (Distinguished Paper Award & Invited to CACM Research Highlights)
  • [POPL ’11] Automating String Processing in Spreadsheets using Input-Output Examples (Invited to CACM Research Highlights)
  • [PLDI ’11] Spreadsheet Table Transformations from Examples (Invited to CACM Research Highlights)
  • [PLDI ’11] Synthesizing Geometry Constructions
  • [PLDI ’11] Synthesis of Loop-Free Programs
  • [PLDI ’11] Path-based Inductive Synthesis for Program Inversion
  • [SAS ’11] Bound Analysis of Imperative Programs with the Size-change Abstraction
  • [OOPSLA ’11] A Simple Inductive Synthesis Methodology and its Applications
  • [PLDI ’10] The Reachability-Bound Problem
  • [POPL ’10] From Program Verification to Program Synthesis
  • [POPL ’10] Continuity Analysis of Programs
  • [PPDP ’10] Dimensions in Program Synthesis (Keynote Paper)
  • [ICSE ’10] Oracle-Guided Component-Based Program Synthesis
  • [ICCPS ’10] Synthesizing Switching Logic for Safety and Dwell-Time Requirement
  • [PLDI ’09] Control-Flow Refinement and Progress Invariants for Bound Analysis
  • [PLDI ’09] Program Verification using Templates over Predicate Abstraction
  • [POPL ’09] SPEED: Precise and Efficient Static Estimation of Program Computational Complexity
  • [POPL ’09] A Combination Framework for Tracking Partition Sizes
  • [CAV ’09] SPEED: Symbolic Complexity Bound Analysis (Keynote Paper)
  • [CAV ’09] VS3: SMT Solvers for Program Verification (Tools Paper)
  • [VMCAI ’09] Constraint-based Invariant Inference over Predicate Abstraction
  • [VMCAI ’09] Synthesizing Switching Logic using Constraint Solving (Journal version appears in STTT 11]
  • [PLDI ’08] Program Analysis as Constraint Solving
  • [PLDI ’08] Inferring Locks for Atomic Sections
  • [CAV ’08] A Numerical Abstract Domain based on Expression Abstraction and Max Operator with Application in Timing Analysis
  • [CAV ’08] Constraint-based Approach for Analysis of Hybrid Systems
  • [CAV ’08] Proving Conditional Termination
  • [ESOP ’08] Cover Algorithms and their Combination
  • [ESOP ’08] Ranking Abstractions
  • [POPL ’08] Lifting Abstract Interpreters to Quantified Logical Domains
  • [POPL ’07] Program Verification as Probabilistic Inference
  • [CAV ’07] An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
  • [ESOP ’07] Computing Procedure Summaries for Interprocedural Analysis
  • [VMCAI ’07] Assertion Checking Unified
  • [PLDI ’06] Combining Abstract Interpreters
  • [ESOP ’06] Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions
  • [Ph.D. Dissertation ’05] Program Analysis using Random Interpretation (Winner of the ACM SIGPLAN Doctoral Dissertation Award)
  • [POPL ’05] Precise Interprocedural Analysis using Random Interpretation
  • [POPL ’04] Global Value Numbering using Random Interpretation
  • [SAS ’04] A Polynomial-Time Algorithm for Global Value Numbering (Journal version appears in Science of Computer Programming, 2007)
  • [SAS ’04] Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions
  • [FSTTCS ’04] Join Algorithms for the Theory of Uninterpreted Functions
  • [POPL ’03] Discovering Affine Equalities using Random Interpretation
  • [CADE ’03] A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols (Journal version appears in Information and Computing 2005)
  • [WCW ’00] WebCaL: A Domain Specific Language for Web Caching

Internships

Microsoft Research (Redmond) Sep-Oct, 2004

  • Mentor: Madan Musuvathi and Tom Ball
  • Project: Combination of cover algorithms.

Microsoft Design and Development (Redmond), Jun-Aug 2001

  • Project: Translation validation for Visual C++ compiler using random interpretation.

IRISA-INRIA labs (Rennes, France), Jun-Aug, 1999

  • Mentor: Gilles Muller and Charles Consel
  • Project: Design and development of a domain specific language for web caching.

Projects

Professional Activities

Current:

Past:

Invited Talks

  • Keynote at MAPL 2017
  • Programming by Examples: Applications, Algorithms, and Ambiguity Resolution, Lectures at UPMARC Summer School, June 2017 [ppt]
  • Programming using Examples, Tutorial at PLDI 2016 [ppt]
  • Spreadsheet Programming using Examples, Keynote at SEMS 2016 [ppt]
  • Programming by Examples: Applications, Algorithms, and Ambiguity Resolution, Invited talk at IJCAR 2016, June 2016
  • Programming by Examples: Applications, Ambiguity Resolution, Approach, Lecture at UC-Berkeley, Nov 2015
  • Talks at Dagstuhl seminar on Approaches and Applications of Inductive Programming, Oct 2015
    • Applications to Data Wrangling
    • Deductive Techniques for Synthesis from Inductive Specifications
    • Microsoft PROSE SDK: A Framework for creating Programming-by-example tools
  • Applications of Formal Methods to Data Wrangling and Education, Keynote at CBSoft 2015
  • Programing by Examples, Tutorial at CBSoft, Sep 2015
  • Programming by Examples, Lectures at Marktoberdorf Summer School, Aug 2015
    • Lecture 1: Demos and Ambiguity Resolution
    • Lecture 2: Domain-specific Languages
    • Lecture 3: Search Methodology
    • Lecture 4: FlashMeta SDK (given by Alex Polozov)
    • Lecture 5: Miscellaneous
  • Programming by Examples applied to Data Wrangling, Invited talk at SYNT 2015
  • Data Wrangling using Programming by Examples [video], Invited talk at ECOOP, July 2015
  • Data Manipulation using Programming by Examples and Natural Language, Distinguished Lecture Series @ UPenn (April 2015)
  • Automating Repetitive Tasks for the Masses, Keynote at POPL 2015
  • Cultivating Research Taste (illustrated via a journey in program synthesis research) [video], Invited talk at PLMW 2015
  • Applications of Program Synthesis to End-User Programming and Intelligent Tutoring Systems, Invited talk at ILP 2014
  • Problem Generation and Feedback Generation, Invited talk at ASSESS 2014
  • Applications of Program Synthesis to End-User Programming and Intelligent Tutoring Systems, Invited talk at GECCO 2014, Genetic Programming Track (July 12-16)
  • Example-Based Learning in Computer-Aided STEM Education, Keynote at 5th IEEE conference on Technology for Education (T4E), Dec 2013
  • End-User Programming and Intelligent Tutoring Systems, Maryland Distinguished Colloquium, Sep 2013
  • Program Synthesis, Lectures at Marktoberdorf Summer School, Aug 2013
    • Part 1: From Verification to Synthesis
    • Part 2: End-User Programming using Examples and Natural language
    • Part 3: Computer-aided Education
  • Synthesis for Computer-aided Education, ExCAPE Summer School, June 2013
  • Distraction: Biological Synthesis, RiSE Group All-hands Meeting, April 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
  • Usable Synthesis, Invited Talk at Usable Verification Workshop 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
  • The Fixpoint Brush in the Art of Invariant Generation, Invited Talk at WING 2010
  • Component Based Synthesis, Dagstuhl Seminar on Software Synthesis

(December 2009)

  • The Reachability-Bound Problem, Invited Talk at FOPARA 2009
  • Art of Invariant Generation applied to Symbolic Bound Computation [Lecture 1(pdf, video)], [Lecture 2(pdf, video)], [Lecture 3(pdf, video)], [Assignment (pdf)], Lectures at Oregon Summer School 2009
  • The Art of Invariant Generation for Symbolic Loop Bound Analysis, Invited Talk at CAV 2009
  • Logical Abstract Interpretation, Lectures in a class on Program Analysis and Verification at IISc-Bangalore (2007) and UCLA (2008)
  • Program Verification using Probabilistic Techniques, Invited Talk at Workshop on Verified Software: Tools, Techniques, and Experiments (VSTTE), Floc 2006
  • Random Interpretation, Smaller version of Job-interview talk, also given at UW/MSR Summer Institute on Trends in Testing: Theory, Techniques and Tools, 2004

ACM SIGPLAN Robin Milner Young Researcher Award

ACM SIGPLAN Robin Milner Young Researcher Award, 2014

Sumit Gulwani has made pioneering contributions to the field of programming languages, especially in the areas of program analysis and program synthesis. Building on his foundational work in program analysis including using randomized algorithms, improving abstract interpretation, and reasoning about programs as continuous functions, Dr. Gulwani recognized the important connection between program verification and program synthesis. His research has demonstrated that imprecise human intent, in the form of examples, natural language, and other kinds of input, can be transformed into incomplete program specifications, which together with ranking techniques can then be used to synthesize intended programs, empowering users to accomplish complex and repetitive programming tasks without needing any knowledge of programming. His contributions include algorithms for synthesizing string transformation programs by examples, published in POPL 2011, and the technical basis for “Flash Fill”, a new feature shipping in Microsoft’s Excel 2013. He has since then extended this line of algorithmic work to synthesizing programs in several other important domains and also broadly advertised this line of work by publishing in top-tier ACM conferences in various other areas including AI, machine learning, HCI, databases, and knowledge discovery. He has also championed the application of program synthesis techniques to developing intelligent tutoring systems for numerous subject domains including introductory programming, mathematics, logic, and automata theory. The visionary aspects of his work were recently recognized by the CACM Editorial Board when two of his recent papers appeared as CACM Research Highlights in the same issue, and a summary of his work on computer-aided Education was accepted to appear as a CACM article.

In summary, Dr. Gulwani is a highly motivated, creative, and inter-disciplinary researcher whose vision is to empower computer users around the world to be more productive and educated. His insights in using program synthesis to address problems in end-user programming and education will have deep and lasting influence.