[ Saurabh Srivastava ]
Ph.D. Candidate,
|
|
Research/Thesis |
Job Application |
Publications |
Projects |
Talks |
Teaching/Courses |
Research Interests
I am interested in programming languages and software engineering and focus on foundational, yet practical, techniques that facilitate program understanding, improve software reliability, and in general, help in building functionally correct software.
My current focus is on automatic program synthesis and program verification. I am also interested in specification inference and type-based approaches to static analysis. Earlier, I worked on a type-systems based approach to modularity and before that I worked on efficient communication techniques in distributed networks.
Thesis --- Program Analysis and Synthesis as Satisfiability Solving
We claim that satisfiability solving is a very practical way to reason about programs. Satisfiability instances arising out of programs are not the pathologically hard instances one can construct but are, in fact, very easy for current solvers. In particular, we show that programs can be verified---even synthesized---using solvers for satisfiability (SAT and SMT). My dissertation, available in Spring 2010, discusses results supporting this thesis in the following contexts:
- Synthesizing programs, proofs and
specifications
Show details
We show that it may be useful to interpret programs as formulas, under a suitable abstraction, to derive:
- Programs: Writing programs as transition systems and generating correctness (safety and termination) constraints, we realize that statements do not have any special status in the resulting formula. Therefore, we can use fixed-point techniques to synthesize programs. (We use our own powerful fixed-point techniques that we built in another context.) (POPL'10)
- Proofs: The proof of correctness can be derived by interpreting the program states (at each program point) in the formula as unknowns. (PLDI'08, VMCAI'09, PLDI'09, CAV'09)
- Specifications: The input and output specifications can be inferred by interpreting the precondition and postcondition in the formula as unknowns. (PLDI'09)
- Abstraction as the key to practical program synthesis
Show details
Programming, as done by developers, scales due to abstraction, be it as ADTs/libraries (in imperative programming), as types (in functional programming) or as objects (in OO programming). Consequently, automatic program synthesis will only be practical if we synthesize fragments modularly, assuming an abstract specification for lower level code, and by guaranteeing an abstract specification to higher level code. (POPL'10)
- Omnidirectional (direction-agnostic) fixed-point
computation
Show details
Traditional approaches to program understanding (e.g., abstract interpretation, model checking) attempt to emulate the way human's understand programs by traversing the sequence of statements. On the other hand, a machine can do better by accumulating information from various parts in parallel (semantic reduction of local fragments to constraints) and then combining the pieces consistently (constraint solving to yield global program fixed-point).
Based on this observation, we compute fixed-points (invariants) by reducing the problem to satisfiability queries. Fixed-point computation is pervasive in program analysis, be it verification-based or type systems-based—and even outside of computer science, in natural processes etc. Our approach provides an alternative to traditional iterative approaches and leverages the growing availability of computing power and theorem proving technology.
Before our work, there was no satisfactory way of encoding forall-exists formulae arising in program analysis/synthesis, of the form below, as SMT/SAT instances, because of the nested quantification:∃Invariant/Program Statements ∀Variables: (Program Consistency Constraints) We give algorithms for these reductions for linear arithmetic (PLDI'08) and predicate abstraction (VMCAI'09, PLDI'09).
Active Projects
VS3: Verification and Synthesis using
SMT Solvers
(VS3 Project Webpage)
We are developing automatic program synthesis and program
verification tools in this project. Using techniques described in my
thesis we reduce synthesis and verification problems to SMT/SAT
instances and use off-the-shelf SMT solvers to solve them and derive the program
(when synthesizing) or invariants (when verifying).
VS3: Verification and Synthesis using SMT Solvers ('07-present)
In this project we are studying a constraint-based approach to program
analysis. Using the techniques developed in this project, we reduce
program properties to
constraints that can be efficiently solved
using off-the-shelf SMT Solvers, yielding efficient and expressive
program analyses. In contrast to previous approaches that uses
theorem proving to validate we have shown how theorem proving can be
used to instead infer program properties; and with a little bit
more work synthesize the program itself!
VS3 Project Webpage
Tool downloads:
- Synthesis over linear arithmetic (.zip)
- Synthesis over predicate abstraction (.zip)
CMod: Enforcing modularity in C Code ('05-'07)
CMod is a tool written to enforce a modular programming style in C code, to
ensure that modules, when linked together, yield a type correct program. By
enforcing a few non-intrusive rules, CMod
lifts the idiomatic notion of modules in C to the level of a formally sound
separate compilation and linking system. We have shown the viability of the
system over a million lines of open-source C code.
CMod Project Webpage
Resource Allocation in CDMA based Ad hoc Networks ('01-'03)
In this project we developed techniques for more optimally using the wireless bandwidth available by making the MAC layer aware of the underlying CDMA physical layer. Better channel utilization is achieved by integrating information from both layers at the cost of losing the clean separation. Almost all wireless cards have hardwired physical and MAC layers, and therefore this loss of modularity is acceptable.
Entry on DBLP.
Peer-reviewed Conference and Journal Publications
Program Inversion Revisited
Saurabh Srivastava and Sumit Gulwani and Swarat Chaudhuri and Jeffrey S. Foster
In preparation
From
Program Verification to Program Synthesis
Saurabh Srivastava and Sumit Gulwani and Jeffrey S. Foster
To appear: Principles of Programming Languages 2010 (POPL'10)
[
bib |
acm |
.ps |
.pdf
]
VS3: SMT Solvers for
Program Verification
Saurabh Srivastava and Sumit Gulwani and Jeffrey S. Foster
Computer Aided Verification 2009 (CAV'09:
Tools Paper)
[
bib |
.ps |
.pdf
]
Program Verification using Templates
over Predicate Abstraction
Saurabh Srivastava and Sumit Gulwani
Programming Languages Design and Implementation 2009 (PLDI'09)
[
bib |
acm |
.ps |
.pdf
]
Constraint-based Invariant Inference over
Predicate Abstraction
Sumit Gulwani and Saurabh Srivastava and Ramarathnam Venkatesan
Verification Model Checking and Abstract Interpretation 2009 (VMCAI'09)
[
bib |
acm |
.ps |
.pdf
]
Program Analysis as Constraint Solving
Sumit Gulwani and Saurabh Srivastava and Ramarathnam Venkatesan
Programming Languages Design and Implementation 2008 (PLDI'08)
[
bib |
acm |
.ps |
.pdf
]
Modular Information Hiding and Type
Safe Linking for C
Saurabh Srivastava and Mike Hicks and Jeffrey S. Foster and Patrick Jenkins
Journal Publication:
IEEE Transactions on Software Engineering 2008 (TSE'08)
[
bib |
acm |
.ps |
.pdf
]
Modular Information Hiding and Type
Safe Linking for C
Saurabh Srivastava and Mike Hicks and Jeffrey S. Foster
Types in Language Design and Implementation 2007 (TLDI'07)
[
bib |
acm |
.ps |
.pdf
]
Distributed Algorithms for Finding and
Maintaining a k-Tree Core in a Dynamic Network
Saurabh Srivastava and R. K. Ghosh
Journal Publication:
Information Processing Letters 2003 (IPL'03)
[
bib |
acm |
.ps |
.pdf
]
A Code Allocation Protocol for Maximizing Throughput in CDMA based Ad-hoc Networks
Saurabh Srivastava and S. Tripathi and A. K. Chaturvedi and D. Sanghi
IEEE Wireless Communications and Networking Conference 2003 (WCNC'03)
Cluster based Routing using a k-Tree Core Backbone for Mobile Ad-hoc Networks
Saurabh Srivastava and R. K. Ghosh
6th International Workshop on Discrete Algorithms and Methods for Mobile
Computing and
Communications 2002 (DialM'02)
Approximating the Range Sum of a Graph on a CREW PRAM
Saurabh Srivastava and P. Gupta
4th Intl. Workshop on Distributed Computing 2002 (IWDC'02)
Performance Evaluation of Combining Techniques for a Multicarrier CDMA System
S. Tripathi and Saurabh Srivastava and A. K. Chaturvedi and D. Sanghi
8th National Conference on Communications 2002 (NCC'02)
Technical Reports
Proof-theoretic Program Synthesis: From Program Verification to Program Synthesis
Saurabh Srivastava and Sumit Gulwani and Jeffrey S. Foster
(To appear jan 1, 2010).
Program Verification using Templates over Predicate Abstraction
Saurabh Srivastava and Sumit Gulwani
MSR-TR-2008-173, Microsoft Research, Redmond, Nov 2008.
Constraint-based Invariant Inference over Predicate Abstraction
Sumit Gulwani and Saurabh Srivastava and Ramarathnam Venkatesan
MSR-TR-2008-163, Microsoft Research, Redmond, Oct 2008.
Program Analysis as Constraint Solving
Sumit Gulwani and Saurabh Srivastava and Ramarathnam Venkatesan
MSR-TR-2008-44, Microsoft Research, Redmond, Oct 2007.
Appendix to CMod: Modular Information Hiding and Type-Safe Linking for C
Saurabh Srivastava and Mike Hicks and Jeffrey S. Foster
CS-TR-4874, Department of Computer Science, UMD, June 2007.
Defining and Enforcing C's Module System
Saurabh Srivastava and Mike Hicks and Jeffrey S. Foster and Bhargav Kanagal
CS-TR-4816, Department of Computer Science, UMD, July 2006.
Information Flow Security using Program Partitioning and Encryptable Functions
Saurabh Srivastava and Mike Hicks
CS-TR-4887, Department of Computer Science, UMD, 2006.
Stability of P2P Networks: A Choas Theoretic Perspective
Saurabh Srivastava
CS-TR-4886, Department of Computer Science, UMD, 2006.
Resource Optimization in CDMA based Wireless Ad Hoc Networks
IIT Kanpur BTech. Thesis 2002 [ abstract
| .ps.gz
| .pdf ]
Advisors: Dheeraj
Sanghi, Ajit K. Chaturvedi
Awarded one of the two best BTech. Projects for the year
2002
PRAM Simulations: General Purpose Parallel Computing on Realistic Parallel Machines
IIT Kanpur Tech. Report 2002 [ .ps.gz ]
VS3
- "Program Synthesis using SMT Solvers", Dagstuhl Software Synthesis Seminar'09, Dec 6-12, 2009.
- "VS3: SMT Solvers for Program Verification", CAV'09, July 1st, 2009.
- "Program Verification and Synthesis Using Templates over Predicate
Abstraction",
- Cambridge University, June 22nd, 2009
- EPFL, June 25th, 2009.
- "Program Verification Using Templates over Predicate Abstraction", PLDI'09, June 17th, 2009.
- "Constraint-based Invariant Inference over Predicate Abstraction", VMCAI'09, Jan 20th, 2009.
- "Constraint-based Approach to Program Analysis", IBM PL Day/NJPLS, Aug, 2008.
- "Constraint-based Analysis over Linear Arithmetic and Predicate Abstraction", MSR India, Feb, 2008.
CMod
- "Modular Information Hiding and Type-Safe Linking for C", TLDI, 2007.
- Part of "Improving Software Quality with Static Analysis", PASTE, 2007.
- "Defining and Enforcing C's Module System", Maryland Software Chat Seminar, Oct, 2006.
- "CMod - A module system for legacy C programs", NJPLS, Oct 2006.
Teaching
Guest Lectures:
- Axiomatic Semantics (CMSC631: Program Analysis and Understanding, Spring 09)
- Memory Management (CMSC412: Operating Systems, Spring 06)
Teaching Assistant:
- CMSC 412: Operating Systems (Spring 06) : Teaching TA for the projects (45% of the course grade)
- CMSC 412: Operating Systems (Fall 05): Teaching TA for the projects (45% of the course grade)
- CMSC 414: Network Security (Spring 05)
- CMSC 417: Computer Networks (Fall 04)
- CMSC 417: Computer Networks (Spring 04)
- CMSC 351: Algorithms (Fall 03)
Graduate Courses Taken
- Randomness and Computation (Spring 07)
- Computational Geometry (Fall 05)
- Chaos Theory (Fall 05)
- Language based Security (Spring 05)
- Combinatorics and Graph Theory (Spring 05)
- Program Analysis and Understanding (Fall 04)
- Intro to Computational Linguistics (Fall 04)
- Advanced Computer Networks (Spring 04)
- Advanced Topics in Computer Systems (Spring 04)
- Distributed Algorithms and Verification (Fall 03)
- Advanced Algorithms (Fall 03)
I am looking for faculty, research lab, post-doc positions starting Summer/Fall 2010.
Application Material
Selected Representative Publications
For the full list see the publications tab.
- Program Inversion Revisited, In preparation
- From Program Verification to Program Synthesis, POPL, 2010
- Program Verification using Templates over Predicate Abstraction, PLDI, 2009
- Program Analysis as Constraint Solving, PLDI, 2008
- Modular Information Hiding and Type Safe Linking for C, TSE Vol 34(3), 2008