Sumit Gulwani 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 ]

Projects

• SPEED: Symbolic Time/Space Bounds Analysis
• VS3: Verification and Synthesis using SMT Solvers
• Logical Abstract Interpretation
• Random Interpretation
(Past Project)

Selected Invited Talks

• 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)
• PC Member: POPL 2011, PLDI 2010, VMCAI 2010, ESOP 2010, PLDI 2009 SRC, SAS 2009, CC 2008
• Workshop Organizer
  • 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.
• Invited Talks: FOPARA 2009, CAV 2009, HAV 2008, VSTTE 2006, UW/MSR Summer Institute on Trends in Testing 2004
• Invited Lectures:
  • 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

Recent/Selected Publications

• From Program Verification to Program Synthesis, POPL 2010, Saurabh Srivastava and Sumit Gulwani and Jeff Foster
  [abstract |ps |pdf]
• Continuity Analysis of Programs, POPL 2010, Swarat Chaudhuri and Sumit Gulwani and Roberto Lublinerman
  [abstract |ps |pdf]
• SPEED: Symbolic Complexity Bound Analysis , Invited Talk Paper, CAV 2009, Sumit Gulwani
  [abstract |ps |pdf]
• 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]
• 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 |dvi |bibtex]


• Other Publications

Personal