Mail NEC Laboratories America 4 Independence Way, suite 200, Princeton, NJ 08540 Phone: 6-099-514-820 Personal E-mail: srirams {AT} theory.stanford.edu

¡Hi!

I am a researcher in the System Analysis and Verification Group at NEC Laboratories (formerly NEC Research Inst.) in Princeton, NJ.

While at Stanford, I worked with the reactive systems group. Zohar Manna was my advisor and Henny Sipma was my co-advisor.

Perhaps, you would like to read some of my papers, or read (beyond) the acknowledgements section of my PhD thesis.

Research Interests

I study verification problems (invariance, termination, reachability, liveness, ...) for dynamical systems ranging from imperative programs written in C to continuous systems governed by differential rate laws. A large part of my work consists of automatically inferring useful properties for such programs from their (text) description. My interests also lie in the use of optimization techniques, Algebraic-Geometric methods (Groebner bases, resultants, etc..), and decision procedures for solving verification problems. Recently, I have developed an interest in sampling/estimation from combinatorially hard search spaces, machine learning, and probabilistic inference for tackling verification problems. Some keywords to describe my current research are:

Program Analysis, Software Modelling and Verification: Abstract Interpretation, Numerical Domains, Real-time and Hybrid Systems.

Optimization and Constraint Solving: Mathematical programming applied to verification and discrete control.

CS Theory : Programming Language Theory, Automata, Logic, and Theoretical Computer Science.

The workshop on Numerical Abstractions for Software Abstractions will be organized as part of CAV 2008 . The workshop will be held on July, 8th 2008 at Princeton, NJ. I am co-organizing this with my colleagues Franjo Ivancic and Chao Wang.

The Northeastern Verification Seminar (NEVER) was held at Princeton, NJ on 18th May 2007.

I co-chaired the special formal methods session at the Workshop on Parallel and Distributed Real-Time Systems (WPDRTS), held in Long Beach, CA, 2007 with Ansgar Fehnker .

F-Soft is an analyzer for commercial C programs being developed inside NEC Labs America. I am working this project along with the other members of the software verification group at NEC Labs America.

TimePass is a prototype analyzer for hybrid systems that implements the method described in HSCC 2006 paper. Email if you wish to try it out yourself.

Lola is a circuit monitoring tool that was used to generate the results in our TIME 2005 paper.

The LPInv system generates linear invariants using linear programming. It implements the numerical domain described in our VMCAI'05 paper.

The StInG system analyzes linear transition systems (programs) to generate linear inequality invariants. It was used to generate results for our SAS 2004 paper.