I am employed by Carnegie-Mellon University and I conduct research in software verification within the Robust Software Engineering group in the Intelligent Systems Division at NASA Ames. I received an M.Sc. and Ph.D. from the ECE Department at The University of Texas at Austin.

My main research interest is in static analysis of programs. With Arnaud Venet, we designed a static analyzer for C programs called C Global Surveyor. CGS has already been applied to the flight software of several NASA missions such as Mars missions (MPF, DS1, MER) and some ISS payload software (UPA). I now work closely with Sarah Thompson on a C++ static analyzer based on the LLVM framework.

I also work on autonomous system technology, and especially, how they can be verified and validated. I am the PI on the Universal Decision-layer Executive project (also called PLEXIL) and one of the technical leads on the A4O (Autonomy For Operations) project.

• with A. Venet. “Precise and Efficient Static Array Bound Checking for Large Embedded C Programs.” In Proceedings of Programming Language Design and Implementation (PLDI). Washington, DC, June 2004.
• with D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. S. Pasareanu, A. Venet, W. Visser. "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software." In Proceedings of the SEI Software Model Checking Workshop. Pittsburgh, PA, 24 March 2003.
• with R. Klemm. “Static Analysis of the Mars Exploration Rover flight software”. In the 1st International Space Mission Challenge for Information Technology, pp. 321-326. Pasadena, California, July 2003.
• with Willem Visser. "Combining Static Analysis and Model Checking for Software Analysis". In 16th International Conference on Automated Software Engineering (ASE'01). Coronado Island, California, November 26-29, 2001.
• with K. Havelund, S.J.. Park, and W. Visser. "Model Checking Programs". In International Conference on Automated Software Engineering. September 2000.
• with S.J. Park, K. Havelund, and W. Visser. "Java PathFinder-Second Generation of a Java Model Checker". In Post-CAV Workshop on Advances in Verification. July 2000