[ Saurabh Srivastava ]
PhD 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 verification, synthesis and specification inference of software systems. Earlier I worked on a type-systems based approach to modularity. In the past, I was interested in algorithmic issues in distributed systems.
Thesis --- Program Analysis and Synthesis as Satisfiability Solving
We claim that satisfiability solving is a very practical way to reason about programs. In particular, we show that programs can be verified, and synthesized (!), using solvers for satisfiability. My dissertation, available in Spring 2010, discusses results supporting this thesis in the following contexts:
- Synthesizing programs, proofs and
specifications:
We show that it may be useful
to interpret programs as formulas, under a suitable abstraction, to derive:
- Programs: Programs can be synthesized by interpreting the statements in the formula as unknowns. (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:
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:
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, of the form below, as SMT instances, because of the nested quantification:∃Invariant ∀Variables: (Program Consistency Constraints) We give algorithms for these reductions for linear arithmetic (PLDI'08) and predicate abstraction (VMCAI'09, PLDI'09).
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
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
From
Program Verification to Program Synthesis
Saurabh Srivastava and Sumit Gulwani and Jeffrey S. Foster
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
Types in Language Design and Implementation 2007 (TLDI'07)
[
bib |
acm |
.ps |
.pdf
]
Journal
Modular Information Hiding and Type
Safe Linking for C
Saurabh Srivastava and Mike Hicks and Jeffrey S. Foster and Patrick Jenkins
IEEE Transactions on Software Engineering 2008 (TSE)
[
bib |
acm |
.ps |
.pdf
]
Distributed Algorithms for Finding and
Maintaining a k-Tree Core in a Dynamic Network
Saurabh Srivastava and R. K. Ghosh
Information Processing Letters (IPL)
[
bib |
acm |
.ps |
.pdf
]
Technical Reports
Proof-theoretic Program Synthesis: From Program Verification to Program Synthesis
Saurabh Srivastava and Sumit Gulwani and Jeffrey S. Foster
(To appear Dec 1, 2009).
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.
Undergraduate Research: Systems (Peer-reviewed)
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)
Undergraduate Research: Systems (Technical Reports)
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
- "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.
Selected Representative Publications
For the full list see the publications tab.
- 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
Application Material
To come -- Dec'09.