Contact
|
|
Research
I am an assistant professor in the Computer Science department at the University of Colorado at Boulder.
Previously, I was a member of research staff at NEC Laboratories America from 2005-2009. I graduated with a PhD in Computer Science from Stanford University in 2005.
A list of my papers is available. Here is a link to my PhD thesis.
Research Interests
My primary research interests lie in the area of mathematical theory of computation, i.e, modeling and reasoning about different forms of (expressing) computation. My work utilizes advanced mathematical techniques to automatically prove that systems are correct , or otherwise find defects in them. I have worked on verification of computer programs for finding defects such as buffer overflows, pointer errors, race conditions, deadlocks and various forms of security violations due to design and coding defects.
My current research considers hybrid systems which are models of programs interacting with a physical environment modeled commonly as differential equations. Simulink/Stateflow models(tm), commonly used in controller design, are examples of this model of computation. Verification techniques for these models is a very important challenge that drives my research. Research in this area is a very interesting combination of ideas from formal methods as well as control theory. My emerging interests lie in understanding the actions of human operators inside interactive systems.
My approach to these problems tends to be very mathematical. I am deeply interested in many areas including logic, convex optimization, algebraic geometric methods, combinatorial optimization, symbolic and numerical decision procedures. Recently, I have taken an interest in statistics, esp. in Monte-Carlo techniques, rare-event simulations and extremal value theory. I also dabble in machine learning from time to time.
Teaching
Events
Program Commitee member of NSAD-2010 , ICSE 2010 (new and emerging research track) and HSCC 2010 part of CPSWeek 2010.
Guest editor (along with Eric Goubault, Georgios Fainekos and Franjo Ivancic) of ACM Transactions of Embedded Systems on Verification of Cyber Physical Software.
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.