I am doing research in software engineering at NASA Ames, in the Robust Software Engineering group. I am employed by Carnegie Mellon University, at the Silicon Valley campus. I am affiliated with CMU CyLab and also hold a courtesy appointment with CMU ECE. Research interests: Model checking and automated testing: I investigate the use of abstraction and symbolic execution in the context of Java PathFinder, with applications to test input generation and error detection. Together with many collaborators, I have developed Symbolic PathFinder (SPF, jpf-symbc), a symbolic execution tool for Java bytecode. See NASA article on the use of SPF in industry. Compositional verification: I also work on using learning and abstraction techniques for automating assume-guarantee style compositional verification. Recently I have worked on compositional techniques for probabilistic systems and I am currently investigating hybrid systems. Model-based development: Together with collaborators from Vanderbilt University and University of Minnesota, we have developed modeling and analysis techniques for multiple statechart formalisms used in the development of NASA systems. See the Polyglot tool-set. Probabilistic software analysis: Recently I have started to investigate probabilistic techniques for the analysis of software components placed in stochastic environments. See project webpage. Autonomy: I was part of the core team that developed PLEXIL, a plan execution language and system for automation. I am now interested in planning for safe surface operations for autonomous vehicles.