Contact
|
|
Research
I am currently a researcher at the System Analysis and Verification Group at NEC Laboratories (formerly NEC Research Institute) at Princeton, NJ.
Starting Aug. 2009, I will be joining the CS department at the University of Colorado at Boulder as an Asst. Professor.
While at Stanford, I worked with the reactive systems group. Zohar Manna was my advisor and Henny Sipma was my co-advisor.
A list of my papers is available. Here is a link to my PhD thesis.
Research Interests
I investigate verification and analysis problems for a variety of dynamical systems ranging from C programs to hybrid control system models governed by differential rate laws (eg., Simulink/Stateflow models). A large part of my work consists of automatically inferring useful properties for such systems from their (text) descriptions. I am also interested in applying ideas from verification to design, esp. of embedded and concurrent systems.
My research utilizes optimization techniques (eg., Linear Programming, Semi-Definite Programming, and so on), Algebraic-Geometric methods (eg., Groebner bases, resultants, etc..), and decision procedures for solving verification problems.
Recently, I have become interested in sampling/estimation from combinatorially hard search spaces (eg., Monte-Carlo methods ), machine learning (eg., Decision Trees , Inductive Logic Programming, and so on ) and probabilistic inference (eg., Language Learning ) for tackling hard verification problems.
Some keywords to describe my current research are:
- Program Analysis, Software Modelling and Verification: Numerical Domains (Convex Polyhedra), Real-time and Hybrid Systems.
- Optimization and Constraint Solving: Optimization techniques applied to verification and discrete control.
- CS Theory : Programming Language Theory, Automata, Logic, and Theoretical Computer Science.
Events
I am co-organizing NSV-II workshop to be held as a part of CPSWeek 2009 on April 16th. The second workshop will focus on numerical verification of control software systems. I will be a co-organizer with Eric Goubault (CEA France) and Georgios Fainekos (NEC Labs).
Program Committee Member of HSCC 2009 to be held in San Francisco, March 2009 as a part of Cyber Physical Systems Week (CPSWeek).
The post proceedings for NSV 2008 will appear as a special issue in the journal Formal Methods in Systems Design.
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 .
Software Projects
F-Soft is an analyzer for commercial C programs being developed inside NEC Labs America. It combines static analysis using numerical-domain abstract interpretation techniques along with model checking based on SAT and SMT solvers. I am working this project along with the other members of the software verification group at NEC Labs America. We are currently extending F-Soft for the analysis of control software.
VARVEL is an interactive verification tool based on F-Soft that is being developed jointly with NEC Japan.
SpecTackle is an annotation inference assistant to F-Soft/Varvel. It helps developers automatically infer annotations for their libraries using static analysis. Our ICSE'08 and ISSTA'08 papers address specification inference using machine learning and dynamic analysis.
CoBE (COncurrency Bug Eliminator) combines static analysis of concurrent programs with powerful model checking techniques for detection of common concurrent program errors such as deadlocks, races, "TOCTOU" bugs and so on. Our CAV 2007 and upcoming TACAS 2009 papers describe some key static analyses behind CoBE. More details are available here
I collect the NEC Small Static Analysis Benchmarks for Static Analysis (mostly Buffer Overflow Analysis) that are available from the NEC Laboratories Site. Other F-Soft benchmarks are available here . Our SAS'07 and SAS'08 papers report the performance of F-Soft on these examples.
TimePass is a prototype analyzer for hybrid systems using symbolic model checking (may also be cast abstract interpretation without widening). Our HSCC 2008 and TACAS 2008 papers extend TimePass to template polyhedra using guaranteed set-valued integration over template polyhedra and policy iteration.
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.