I am an assistant professor in the Computer Science department at the University of Colorado at Boulder. I am a member of the Programming Languages & Verification and Computer & Cyber-Physical Systems research groups. 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. Here is a link to a brief biography.
Simply put, I am interested in automatically proving programs correct or finding bugs in them. As a rule, such problems are undecidable , i.e., they cannot be solved in their full generality using a computer. Discovering ways to reformulate the problem (eg., find techniques to automatically discover simpler abstractions of a given program), and focusing on special but useful cases can still help us tackle many practical software systems.
My focus is on reasoning about hybrid dynamical (cyber-physical) systems, which model discrete programs interacting with a continuous environment modeled by ordinary differential equations (ODEs).
This research is part of the larger areas of Automata Theory, Logic and Formal Languages. My research naturally lends itself to techniques from diverse areas such as convex optimization, algebraic geometric methods, combinatorial optimization, Monte-Carlo techniques (rare-event simulation), symbolic and numerical decision procedures.
Infusion Pump analysis project looks at the model-based analysis of human interaction with medical devices. The focus is specifically on infusion pumps (drug infusion pumps and insulin infusion pumps).
Flow* a Taylor model-based flowpipe construction for non linear hybrid systems.
Symbolic Verification of Hybrid systems: A compendium of our work and supplmentary materials for this topic.
Digital Filter verification project. Our work focuses on analyzing overflow errors in fixed point digital filter implementations.
Relational abstractions for hybrid systems (joint work with Aditya Zutshi and Ashish Tiwari). Benchmarks available from our project page. Tool will be released upon request.
S-Taliro is a Matlab toolbox for evaluating rare-event simulation techniques for testing Simulink/Stateflow diagram. This tool is part of the Taliro framework designed by Georgios Fainekos and his students at Arizona State University.
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.
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. Even though, we found dynamic analysis approaches to be good for likely invariant annotations, SpecTackle used a purely static approach to obtain preconditions that compared quite favorably with manually written annotations.
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 have collected 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.
Aleksandar Chakarov (PhD student, CSCI).
Arlen Cox (PhD student, ECEE. Co-advised with Evan Chang).
Hadi Ravanbakhsh (PhD student, CSCI).
Yan Zhang (PhD student, ECEE. Co-advised with Fabio Somenzi).
Aditya Zutshi (PhD student, ECEE).
Ranga Ragunathan (MS, ECEE).
Nathan Lapinski (Undergraduate, CSCI).
Paul Givens (Undergraduate, CSCI)
Christopher Miller (Undergraduate, Mechanical Engineering)
Huxley Bennett (MS 2012).
Hadjar Homaie (MS, 2011).
Sidartha Gracias (MS, 2011).
Aaron Schlicht (ME, 2011).
Program Commitees: NASA Formal Methods Symposium (NFM) 2013 , HSCC 2013 , SAS 2012 , CAV 2012, HSCC'12, VMCAI 2012, LCPC 2011 , MACIS 2011 , APLAS'11, Workshop on Safety and Security in Cyber-Physical Systems, CAV 2011, VMCAI 2011, NSV-3 , NSAD-2010 , ICSE 2010 (new and emerging research track) and HSCC 2010 part of CPSWeek 2010 and HSCC 2009 as a part of Cyber Physical Systems Week (CPSWeek 2009).
Guest editor (along with Eric Goubault, Georgios Fainekos and Franjo Ivancic) of ACM Transactions of Embedded Systems on Verification of Cyber Physical Software.
NSV Workshops: NSV 2012 was held as part of CAV 2012 in Berkeley, CA. I co-organized it with Prof. Swarat Chaudhuri. NSV4 held as part of CAV 2011 in Snowbird Utah. I will be a co-organizer with Drs. Eric Goubault, Sylvie Putot and Prof. Stefan Ratschan.
Co-organized NSV-II workshop held as a part of CPSWeek 2009 on April 16th. The second workshop will focus on numerical verification of control software systems. Other organizers included Eric Goubault (CEA France) and Georgios Fainekos (NEC Labs).
The workshop on Numerical Abstractions for Software Abstractions was organized as part of CAV 2008 . The workshop was held on July, 8th 2008 at Priceton, NJ. Co-Organizers: 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 .