My current research interests are in the areas of automated program synthesis and
quantitative program analysis (including symbolic computational complexity analysis,
resource bound analysis, analysis of uncertain/approximate computation). I have always been interested in
art of invariant generation. My work has drawn on techniques from formal verification
(logic, theorem proving, and model checking), randomized algorithms, and machine learning.
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.
The Reachability-Bound Problem
[ppt],
Invited Talk at FOPARA 2009
Art of Invariant Generation applied to Symbolic Bound Computation
[Lecture 1,
Lecture 2,
Lecture 3],
Lectures at Oregon Summer School 2009 (Extended version of CAV 2009 talk below)
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
Students (co-advised by me):
Saurabh Srivastava (University of Maryland at College Park),
Sagar Jain (IIT Kanpur)
VS3: SMT Solvers for Program Verification
,
Tools Paper, CAV 2009,
Saurabh Srivastava, Sumit Gulwani, and Jeffrey Foster
[abstract
|ps
|pdf]
Control-Flow Refinement and Progress Invariants for Bound Analysis,
PLDI 2009,
Sumit Gulwani, Sagar Jain, and Eric Koskinen
[abstract
|ps
|pdf]
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]
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]
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
|dvi
|bibtex]