[ Saurabh Srivastava ]
Postdoctoral CI Fellows 2010-12 Researcher,
CS, University of California, Berkeley
(Mentor: Ras Bodik)
Past life: Ph.D., PLUM Group, CS, University of Maryland, College Park
| Email: |
|
esiaduorlaobnh@sE@IcDsO.LbOe.rakpeplleey..CeOdMu
|
| Phone: |
|
(202) 355-8862 |
| Address: |
|
517 Soda Hall, |
|
|
CS Division, Mailing Code 1776 |
|
|
UC Berkeley, Berkeley, CA 94720 |
|
|
About |
Research/Projects |
Publications |
Talks/Other |
I am currently a postdoctoral researcher at UC Berkeley. I spend my days working on program synthesis (with bits of data mining and machine learning thrown in) within the context of an algorithmic synthetic biology project on enzymatic pathway synthesis.
My expertise is in formal methods, synthesis and verification.
My thesis explored SAT/SMT-based techniques for program synthesis and verification, while my postdoc work has been directed towards bringing these techniques to synthetic biology as well as systems biology.
I completed my Ph.D. in programming languages at the University of
Maryland, College Park in May 2010. I had the pleasure of being advised by
Jeffrey S. Foster, and
co-advised by
Sumit Gulwani, and
Michael W. Hicks.
My current research agenda is best summarized by the slide below:
Research Interests
Synthetic biology is the relatively new discipline of genetic modification of
(primarily) bacteria and yeast to endow the organism with rationally designed
unnatural function. Algorithmic techniques to reason about such modifications
are virtually non-existent as of the moment. In what I like to call, algorthmic
synthetic biology, we are building prediction and verification tools for
directing experimental work.
My current focus is on building a synthesizer that can predict genetic
modifications that will allow organisms to feed on sugars and produce 1-butanol
(a biofuel), arbekacin (an antibiotic), or polymers. Additionally, we are
building a verifier that will validate the correctness (both syntactic, at the
DNA level; and semantic, at the protein function level) of synthetic DNA.
My research on programming languages
focuses on foundational, yet practical, techniques that facilitate program
understanding, improve software reliability, and in general, help in
building functionally correct software.
I have developed techniques for 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.
Active Projects
Model synthesizer for systems biology
I work with two great students, Ali Sinan Koksal (Ph.D) and Evan Pu (ugrad), on this project. Here we are developing an semi-automatic model synthesizer that takes as input experimental data, and hints about the biological process to synthesize a formally executable/checkable model of the biological process.
Enzymatic Pathway Synthesizer
Consider the task of generating a particular chemical of interest, e.g., an antibacterial drug or a biofuel. Either it can be done through traditional, expensive, chemical synthesis processes or it can be biosynthesized. While most chemicals are not naturally synthesized, new PCR and DNA synthesis technology allows experimentalists to inject E. coli or Yeast with DNA that allows the organism to do complicated chemistry using enzymes that it produces as a consequence of the new DNA.
Our task in this project is to generate operators from existing biochemical data, which are then the core operators over which a program is synthesized that when inserted into the E. coli will make it a "chemical microbial factory".
Pathway Sythesis Blog
Synthetic Biology Verfier
Current synthetic biology is built around discover-(build-test)* cycles. The discover step is accomplished by experimentalists trolling the literature tomes. In our pathway synthesis project we are attempting to automate that task. The build-test cycles are expensive wet-lab processes that sometimes fail due to bad sequence data and lack of understanding of molecular interactions between components. In our verifier project we take a candidate sequence that the experimentalist intends to build in the lab, and run it through a computational verification process that infers the likelihood of the sequence succeeding.
Act Verifier
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).
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!
Tool downloads:
- Synthesis over linear arithmetic (.zip)
- PINS:
Path-based Inductive Synthesis
VS3 was part of my Ph.D. [ Satisfiability-based Program Reasoning and Program Synthesis ]
Download:
- Tree-friendly print version: 9pt .pdf
- Eye-friendly screen reading version: 12pt .pdf
Show
abstract.
Program reasoning consists of the tasks of automatically and statically verifying correctness and inferring properties of programs. Program synthesis is the task of automatically generating programs. Both program reasoning and synthesis are theoretically undecidable, but the results in this dissertation show that they are practically tractable. We show that there is enough structure in programs written by human developers to make program reasoning feasible, and additionally we can leverage program reasoning technology for automatic program synthesis.
This dissertation describes expressive and efficient techniques for program reasoning and program synthesis. Our techniques work by encoding the underlying inference tasks as solutions to satisfiability instances. A core ingredient in the reduction of these problems to finite satisfiability instances is the assumption of templates. Templates are user-provided hints about the structural form of the desired artifact, e.g., invariant, pre– and postcondition templates for reasoning; or program templates for synthesis. We propose novel algorithms, parameterized by suitable templates, that reduce the inference of these artifacts to satisfiability.
We show that fixed-point computation—the key technical challenge in program reasoning—is encodable as SAT instances. We also show that program synthesis can be viewed as generalized verification, facilitating the use of program reasoning tools as synthesizers. Lastly, we show that program reasoning tools augmented with symbolic testing can be used to build powerful synthesizers with approximate guarantees.
We implemented the techniques developed in this dissertation in the form of the VS3—Verification and Synthesis using SMT Solvers—suite of tools. Using the VS3 tools, we were able to verify and infer expressive properties of programs, and synthesize difficult benchmarks from specifications. These prototype tools demonstrate that we can exploit the engineering advances in current SAT/SMT solvers to do automatic program reasoning and synthesis. We propose building future automatic program reasoning and synthesis tools based on the ideas presented in this dissertation.
Show
ideas covered in the dissertation.
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 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).
Past Projects
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.
Collaborators/Students
Collaborators:
Student collaborators:
- Ali Sinan Koksal (PhD, EECS)
- Jon Kotker (MS, EECS)
- Tim Hsiau (PhD, Bioengg)
- Bhargav Kanagal (PhD, CS@UMD now at Yahoo Research)
- UG: Evan Pu, Stephi Hamilton, Paul Ruan, and Jeff Tsui
Author page on ACM, and DBLP.
Peer-reviewed Conference and Journal Publications
Template-based Program Verification and Program Synthesis
Saurabh Srivastava and Sumit Gulwani and Jeffrey S. Foster
Journal on Software Tools for Technology Transfer 2012 (STTT'12)
[
bib | .ps | .pdf
]
Synthesis of first-order dynamic programming algorithms
Yewen Pu, Rastislav Bodik, Saurabh Srivastava
Object Oriented Programming, Systems, Languages, and Applications 2011(OOPSLA'11)
[
bib | .ps | .pdf
]
Parallel Programming with Inductive Synthesis
Shaon Barman, Rastislav Bodik, Sagar Jain, Yewen Pu, Saurabh Srivastava, Nicholas Tung
Hot Topics in Parallel Computing 2011(HotPar'11)
[
bib | .ps | .pdf
]
Path-based Inductive Synthesis for Program Inversion
Saurabh Srivastava and Sumit Gulwani and Swarat Chaudhuri and Jeffrey S. Foster
Programming Languages Design and Implementation 2011 (PLDI'11)
[
bib |
acm |
.ps |
.pdf |
talk pdf
]
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 |
talk 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 |
talk 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 |
talk 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 |
talk 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 |
talk 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 |
talk 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 ]
Talks
Algorithmic Synthetic Biology
- "Algorithmic Synthesis for Synthetic Biology," [ .key | .pdf ] and "Data repair using I-O Witnesses: A challenge problem from enzymology," [ .key ], Dagstuhl Seminar on Program Synthesis, Apr 2012.
- "Enzymatic Pathway Synthesis," [.key | .pptx ] OSQ discussion, Mar 2012.
- "Synthetic Biology as Programming Languages," [.key | .pptx ] UCB PL Graduate Student visit day. Short project overview talk, Mar 2012.
VS3
- "Satisfiability-based Program Reasoning and Synthesis", [ .ppt ]
- University of California, Berkeley, May, 2010.
- Microsoft Research, May, 2010.
- IMDEA Software, Mar, 2010.
- Ohio State University, Feb, 2010.
- "Program Synthesis using SMT Solvers", [ .ppt ]
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", [ .ppt ]
- Cambridge University, June 22nd, 2009
- EPFL, June
25th, 2009.
- "Program Verification Using Templates over Predicate
Abstraction", [ .ppt ]
PLDI'09, June 17th, 2009.
- "Constraint-based Invariant Inference over Predicate Abstraction", [ .ppt ]
VMCAI'09, Jan 20th, 2009.
- "Constraint-based Approach to Program Analysis", [ .ppt ] 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.
Service
Program Committee and Reviewer
- Program Committee: BSD (Biological Systems Design) 2012, VMCAI 2013
- Reviewer: CAV 2012, CC 2012, STTT 2012, SAS 2011, POPL 2011, VMCAI 2011, POPL 2009, PLDI 2009, SAS 2009,
JSC (Journal on Symbolic Computation, special issue on Invariant Geneneration),
ESOP 2009,
COORD 2008
- Graduate admissions committee UMD, 2008
Teaching
Guest Lectures:
Teaching Assistant:
Friends
(SEO for friends) Check out Indigo Contemporary Arts.
|
