NASA Logo, National Aeronautics and Space Administration

Guillaume Brat

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.

I am Principal Systems Scientist at CMU Silicon Valley serving as an IPA at NASA Ames Research Center. I have been the Assistant Area lead for Robust Software Engineering since October 2009. The group conducts research on new verification and validation techniques, mostly based on formal methods.

I am also Project Scientist for the System-wide Safety Assurance Technologies (SSAT) project in the Aviation Safety program in ARMD. I am focusing on the largest theme of the project, the Assurance of Flight Critical Systems (AFCS). Within AFCS, I set research directions for the Software Intensive Systems and Authority & Autonomy elements, for which most of the research is done in RSE at NASA ARC. SSAT is an example of center collaboration. We are working very close to researchers at LaRC and DRFC.

As a researcher, I have worked mostly on static analysis of programs. In the past, with Arnaud Venet, we designed a static analyzer for C programs called C Global Surveyor. CGS has been applied to the flight software of several NASA missions such as Mars missions (MPF, DS1, MER) and some ISS payload software (UPA). Since then, under SSAT funding, the team has expanded and we have developed IKOS, a framework for developing static analyzers based on abstract interpretation. The scalability and precision of IKOS have been demonstrated with a buffer-overflow analysis. This analyzer has been released to private industry at the end of 2013.

Other interests of mine include:

  • autonomous system technology
  • human-machine interaction

especially the V&V aspects of these technologies.

Selected publications:

  • 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


Intelligent Systems Division
Ames Research Center
Mail Stop 269-2
Moffett Field, CA 94035

Phone: +1 650-604-1105
Fax: +1 650-604-3594

Email: Guillaume.P.Brat "at"

First Gov logo
NASA Logo -