[

]

Sumit Gulwani's ResumePrimary Affiliation: Senior Researcher @ Microsoft Research (Redmond lab)

Other Affiliations: Adjunct Faculty @ IIT Kanpur

Affiliate Faculty @ University of Washington

Address: Microsoft Corporation, One Microsoft Way,

Redmond, WA, 98052

Email: abqf33@r.postjobfree.com

Phone:

+1-425-***-****

Homepage: http://research.microsoft.com/users/sumitg/

Employment and EducationSenior Researcher (June 2011 - present)

Microsoft Research, Redmond, USAResearcher (August 2005 - May 2011)

Microsoft Research, Redmond, USAPh.D., Computer Science (2000-2005)

University of California at

Berkeley

Advisor: Prof. George NeculaB.Tech, Computer Science and Engineering (1996-2000)

Indian Institute

of Technology (IIT), Kanpur, India

GPA: 4.00AwardsMicrosoft Thought Leadership Award, 2011 (for Office-by-Example technology).Distinguished Paper Award, FSE 2011Microsoft 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 AccomplishmentsAdjunct Faculty Member @ IIT KanpurAffiliate Faculty Member @ Univ. of WashingtonEECS Industrial Advisory Board @ Oregon State UniversityAuthored 25 patent applications (Granted: 5, Under review: 20) and 60+ research papers.Media Articles:

Flash Fill (Excel feature in Office 2013)Ph.D. Students Co-advised:

Saurabh Srivastava (University of Maryland at College Park; now post-doc at UC-Berkeley)Florian Zuleger (TU Vienna; now tenure-track faculty at the same Institute)Rishabh Singh (MIT)Vu Le (UC-Davis)Erik Andersen (University of Washington)Daniel Perelman (University of Washington)Alex Polozov (University of Washington)Program Committee Member: 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:

Workshop on Programming Languages Technology for Massive Open Online Courses, June 2013 (Co-located with PLDI 2013)Dagstuhl Seminar on Software Synthesis, Apr 2012 Dagstuhl Summer School on Software Synthesis, Aug 2011 Workshop on Quantitative Analysis of Software, June 2009 Workshop on Security and Reliability in Software Systems, December 2008Participant 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. Invited Lectures (1 week each) 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 Invited Talks Intelligent Tutoring Systems, Invited Talk at ExCAPE Summer School on Software Synthesis, June 2013Synthesis from Examples: Interaction Models and Algorithms, Invited Talk at SYNASC 2012End 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 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[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[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 CachingInternshipsMicrosoft 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.

Contact this candidate