Sumit Gulwani's Homepage

Sumit Gulwani
Senior Researcher
Microsoft Research (Redmond Lab)
RiSE Group
Email: sumitg at microsoft dot com
Phone: (425) 706-7709
Fax: (425) 936 7329 (attn: sumitg)

[ Biography | Contact Information | Resume ]

My current research interests are in the application areas of automating end-user programming (for a variety of systems such as spreadsheets, databases, smartphones, robots), and in building intelligent tutoring systems (for K-12 math/science/language subjects). I have expertise in automated program synthesis techniques and logic based program analysis techniques. I am also interested in machine learning, natural language processing, and human-computer interaction techniques. 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.

I mentor several Undergraduate, Masters, and Phd students in areas ranging from logics, natural language processing, machine learning, sketch recognition, etc. If you are looking for disruptive project ideas that would contribute to building 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.

Projects

Program Synthesis
Cauchy: Analytical Interpretation
SPEED: Symbolic Time/Space Bounds Analysis
VS3: Template-based Verification and Synthesis using SMT Solvers
Logical Abstract Interpretation
Random Interpretation

Selected Invited Talks

Synthesis from Examples [pdf], Invited Talk at WAMBSE 2012
Usable Synthesis [ppt], Invited Talk at Usable Verification Workshop 2010
Dimensions in Program Synthesis [ppt], Invited Tutorial at FMCAD 2010
Program Synthesis for Automating Education [ppt], Keynote at AVM 2010
Dimensions in Program Synthesis [ppt], Invited Talk at PPDP 2010
The Fixpoint Brush in the Art of Invariant Generation [ppt], Invited Talk at WING 2010
Component Based Synthesis [ppt], Dagstuhl Seminar on Software Synthesis
The Reachability-Bound Problem [ppt], Invited Talk at FOPARA 2009
Art of Invariant Generation applied to Symbolic Bound Computation [Lecture 1(ppt, pdf, video, audio)], [Lecture 2(ppt, pdf, video, audio)], [Lecture 3(ppt, pdf, video, audio)], [Assignment (pdf)], Lectures at Oregon Summer School 2009
The Art of Invariant Generation for Symbolic Loop Bound Analysis [ppt], Invited Talk at CAV 2009
Logical Abstract Interpretation [ppt], Lectures in a class on Program Analysis and Verification at IISc-Bangalore (2007) and UCLA (2008)
Program Verification using Probabilistic Techniques [ppt], Invited Talk at Workshop on Verified Software: Tools, Techniques, and Experiments, Floc 2006
Random Interpretation, [ppt], Smaller version of Job-interview talk, also given at UW/MSR Summer Institute on Trends in Testing: Theory, Techniques and Tools, 2004

Professional Activities

Industrial Advisory Board @ Oregon State University
Media:
Invited Talks: SYNASC 2012, WAMBSE 2012, ISEC 2012, PASTE 2011, AVM/RiSE 2011, FMCAD 2010 Tutorial, AVM 2010, PPDP 2010, WING 2010, FOPARA 2009, CAV 2009, HAV 2008, VSTTE 2006, UW/MSR Summer Institute on Trends in Testing 2004
Invited Lectures:
- Marktoberdorf International Summer School, August 2013
- Summer School on Formal Techniques at Menlo College, Atherton, CA, May 2012
- Summer School on Logic and Theorem-Proving in Programming Languages at University of Oregon, 2009
- Static Program Analysis course at UCLA, 2008
- Program Analysis and Verification course at IISc-Bangalore, 2007
Workshop/Summer-school Organization
- Dagstuhl Seminar on Software Synthesis, Apr 2012.
- Dagstuhl Summer School on Software Synthesis, Aug 2011.
- Workshop on Quantitative Analysis of Software, colocated with CAV 2009, Grenoble, France.
- Workshop on Security and Reliability in Software Systems, colocated with FSTTCS/APLAS 2008, Bangalore, India.
Collaborator on $10 million NSF Expeditions grant: ExCAPE: Expeditions in Computer Augmented Program Engineering
PC Member: CICM 2012, CC 2012, SAS 2011, POPL 2011, PLDI 2010, VMCAI 2010, ESOP 2010, PLDI 2009 SRC, SAS 2009, CC 2008
Students (co-advised by me):
- Current: Vu Le (UC-Davis), Rishabh Singh (MIT), Shachar Itzhaky (Tel-Aviv University)
- Past: Florian Zuleger (TU Vienna), Saurabh Srivastava (University of Maryland at College Park, now post-doc at UC-Berkeley)

Recent/Selected Publications

Synthesis from Examples, WAMBSE 2012 (Invited Talk Paper), Sumit Gulwani
[abstract |pdf |bibtex]

Spreadsheet Data Manipulation using Examples, To appear in CACM 2012, Sumit Gulwani, William Harris, Rishabh Singh
[abstract |pdf]

Continuity and Robustness of Programs, To appear in CACM 2012, Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman
[abstract]

Automatically Generating Algebra Problems, AAAI 2012, Rohit Singh, Sumit Gulwani, Sriram Rajamani
[abstract |pdf |full-version(pdf)]

Learning Semantic String Transformations from Examples, VLDB 2012, Rishabh Singh, Sumit Gulwani
[abstract |pdf]

QuickDraw: Improving Drawing Experience for Geometric Diagrams, CHI 2012, Salman Cheema, Sumit Gulwani, Joseph LaViola
[abstract |pdf]

Synthesizing Number Transformations from Input-Output Examples, CAV 2012, Rishabh Singh, Sumit Gulwani
[abstract |pdf |Full-version(pdf)]

Type-Directed Completion of Partial Expressions, PLDI 2012, Daniel Perelman, Sumit Gulwani, Tom Ball, Dan Grossman
[abstract |pdf]

Template-based Program Verification and Program Synthesis, Journal on Software Tools for Technology Transfer 2012, Saurabh Srivastava, Sumit Gulwani, Jeff Foster
[abstract |pdf] (Final version available at Springerlink)

Proving Programs Robust, FSE 2011, Distinguished Paper Award, Invited to CACM Research Highlights, Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman and Sara Navidpour
[abstract |pdf |slides]

Automating String Processing in Spreadsheets using Input-Output Examples, POPL 2011, Invited to CACM Research Highlights, Sumit Gulwani
[abstract |pdf |ppt slides |video presentation |CACM version(pdf) ]

Spreadsheet Table Transformations from Examples, PLDI 2011, Invited to CACM Research Highlights, William Harris, Sumit Gulwani
[abstract |pdf |ps |Full version pdf |ppt slides |CACM version(pdf)]

Synthesizing Geometry Constructions, PLDI 2011, Sumit Gulwani, Vijay Korthikanti, Ashish Tiwari
[abstract |pdf |ps |ppt slides]

Synthesis of Loop-Free Programs, PLDI 2011, Sumit Gulwani, Susmit Jha, Ashish Tiwari, Ramarathnam Venkatesan
[abstract |pdf |ps |ppt slides]

Path-based Inductive Synthesis for Program Inversion, PLDI 2011, Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, Jeff Foster
[abstract |pdf |ps |pdf slides ]

Bound Analysis of Imperative Programs with the Size-change Abstraction, SAS 2011, Florian Zuleger, Moritz Sinn, Sumit Gulwani and Helmut Veith
[abstract |pdf]

Dimensions in Program Synthesis, PPDP 2010, Sumit Gulwani
[abstract |pdf |ppt slides]

A Simple Inductive Synthesis Methodology and its Applications, OOPSLA 2010, Shachar Itzhaky, Sumit Gulwani, Neil Immerman, and Mooly Sagiv
[abstract |pdf]

Synthesizing Switching Logic for Safety and Dwell-Time Requirement, ICCPS 2010, Susmit Jha, Sumit Gulwani, Sanjit Seshia and Ashish Tiwari
[abstract| pdf| full-version pdf]

The Reachability-Bound Problem, PLDI 2010, Sumit Gulwani and Florian Zuleger
[abstract| ps| pdf]

Oracle-Guided Component-Based Program Synthesis, ICSE 2010, Susmit Jha, Sumit Gulwani, Sanjit Seshia and Ashish Tiwari
[abstract |ps |pdf]

From Program Verification to Program Synthesis, POPL 2010, Saurabh Srivastava and Sumit Gulwani and Jeff Foster
[abstract |ps |pdf |ppt slides]

Continuity Analysis of Programs, POPL 2010, Swarat Chaudhuri, Sumit Gulwani and Roberto Lublinerman
[abstract |ps |pdf]

SPEED: Symbolic Complexity Bound Analysis , Invited Talk Paper, CAV 2009, Sumit Gulwani
[abstract |ps |pdf |ppt slides]

VS3: SMT Solvers for Program Verification , Tools Paper, CAV 2009, Saurabh Srivastava, Sumit Gulwani, and Jeffrey Foster
[abstract |ps |pdf |ppt slides]

Control-Flow Refinement and Progress Invariants for Bound Analysis, PLDI 2009, Sumit Gulwani, Sagar Jain, and Eric Koskinen
[abstract |ps |pdf |pdf slides]

Program Verification using Templates over Predicate Abstraction, PLDI 2009, Saurabh Srivastava and Sumit Gulwani
[abstract |ps |pdf |ppt slides]

SPEED: Precise and Efficient Static Estimation of Program Computational Complexity , POPL 2009, Sumit Gulwani, Krishna Mehra, and Trishul Chilimbi
[abstract |ps |pdf |ppt slides |full-version(pdf)]

A Combination Framework for Tracking Partition Sizes , POPL 2009, Sumit Gulwani, Tal Lev-Ami, and Mooly Sagiv
[abstract |ps |pdf |ppt slides |full-version(pdf)]

Constraint-based Invariant Inference over Predicate Abstraction, VMCAI 2009, Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan
[abstract |ps |pdf |pdf slides]

Synthesizing Switching Logic using Constraint Solving, VMCAI 2009, Ankur Taly, Sumit Gulwani, and Ashish Tiwari
[abstract |ps |pdf |pdf slides |Journal version(STTT 2011)]

A Numerical Abstract Domain based on "Expression Abstraction" and "Max Operator" with Application in Timing Analysis, CAV 2008, Bhargav Gulavani and Sumit Gulwani
[abstract |pdf |ppt slides]

Constraint-based Approach for Analysis of Hybrid Systems, CAV 2008, Sumit Gulwani and Ashish Tiwari
[abstract |pdf |pdf slides]

Proving Conditional Termination, CAV 2008, Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko and Mooly Sagiv
[abstract |pdf]

Program Analysis as Constraint Solving, PLDI 2008, Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan
[abstract |ps |pdf |ppt slides]

Inferring Locks for Atomic Sections, PLDI 2008, Sigmund Cherem, Trishul Chilimbi, and Sumit Gulwani
[abstract |pdf |ppt slides]

Cover Algorithms and their Combination, ESOP 2008, Sumit Gulwani and Madanlal Musuvathi
[abstract |pdf |ppt slides]

Ranking Abstractions, ESOP 2008, Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv and Hongseok Yang
[abstract |ps |pdf |pdf slides]

Lifting Abstract Interpreters to Quantified Logical Domains, POPL 2008, Sumit Gulwani and Bill McCloskey and Ashish Tiwari
[abstract |ps |pdf |ppt slides]

An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software, CAV 2007, Sumit Gulwani and Ashish Tiwari
[abstract |ps |pdf |ppt slides]

Computing Procedure Summaries for Interprocedural Analysis, ESOP 2007, Sumit Gulwani and Ashish Tiwari
[abstract |ps |pdf |pdf slides]

Assertion Checking Unified, VMCAI 2007, Sumit Gulwani and Ashish Tiwari
[abstract |ps |pdf |ppt slides]

Program Verification as Probabilistic Inference, POPL 2007, Sumit Gulwani and Nebojsa Jojic
[abstract |ps |pdf |ppt slides]

Combining Abstract Interpreters, PLDI 2006, Sumit Gulwani and Ashish Tiwari
[abstract |ps |pdf |ppt slides]

Precise Interprocedural Analysis using Random Interpretation, POPL 2005, Sumit Gulwani and George Necula
[abstract |ps |pdf |ppt slides]
Global Value Numbering using Random Interpretation, POPL 2004, Sumit Gulwani and George Necula
[abstract |ps |pdf |ppt slides]
Discovering Affine Equalities using Random Interpretation, POPL 2003, Sumit Gulwani and George Necula
[abstract |ps |pdf |ppt slides]
Program Analysis using Random Interpretation, PhD Dissertation, UC-Berkeley, 2005, Sumit Gulwani, Winner of the ACM SIGPLAN Doctoral Dissertation Award
[abstract |ps |pdf |ppt slides |bibtex]

Other Publications

Personal

Pictures