Affiliate Faculty @ University of Washington [since Fall 2012]

- 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

**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.

- Adjunct Faculty Member @ IIT Kanpur
- Affiliate Faculty Member @ Univ. of Washington
- EECS Industrial Advisory Board @ Oregon State University
- Authored
**37 patent applications**(Granted: 13, Under review: 24) and**80+ research papers**. **Media Articles**:- Best of both worlds: one researcher’s dual approach
- Ode to the Automata Tutor
- FlashExtract (released as part of the Windows Management Framework 5.0 preview) [Video]
- Bing Code Search Makes Developers More Productive
- Flash Fill (Excel feature in Office 2013)
- Flash Fill Gives Excel a Smart Charge
- Computers will raise the IQ of the World
- Programming for Dummies
- Computer Programming Itself
- Excel programming for nonprogrammers
- Automatically grading programming homework (The Auto Grader)
**Ph.D. Students Co-advised**:- Saurabh Srivastava (University of Maryland at College Park; now runs a startup 20n.com)
- Florian Zuleger (TU Vienna; now tenure-track faculty at the same Institute)
- Rishabh Singh (MIT; now Researcher at MSR)
- Vu Le (UC-Davis; now Researcher at Microsoft)
- Erik Andersen (University of Washington; now Assistant Professor at Cornell)
- Daniel Perelman (University of Washington; now at Microsoft)
- Alex Polozov (University of Washington)

**Program Committee Member**: POPL 2016 ERC, PLOOC 2015, AInF 2015, KDD 2015, PLDI 2015 ERC, POPL 2015 ERC, ASSESS 2014, PLOOC 2014, Learning at Scale 2014, PLDI 2014, PLDI 2013 ERC, CICM 2012, CC 2012, SAS 2011, POPL 2011, PLDI 2010, ESOP 2010, PLDI 2009 SRC, SAS 2009, CC 2008**Workshop/Seminar Organization**:- Dagstuhl Seminar on Approaches and Applications of Inductive Programming, Dec 2013
- Workshop on Programming Languages Technology for Massive Open Online Courses (PLOOC), June 2013 (Co-located with PLDI 2013)
- Dagstuhl Seminar on Software Synthesis, Apr 2012
- Workshop on Quantitative Analysis of Software, June 2009
- Workshop on Security and Reliability in Software Systems, December 2008

- Participant on
**NSF Grants**,**NSF Panels**,**DARPA ISAT Meetings**.- Collaborator on $10 million NSF Expeditions grant: ExCAPE: Expeditions in Computer Augmented Program Engineering

- Teaching assistant for upper-division course ``Programming Languages and
Compilers'' (cs164), UC-Berkeley, Spring 2003.

- Member of graduate admissions committee, computer science division, UC-Berkeley, 2004.

*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

*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.

- [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

- 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.