NASA Logo, National Aeronautics and Space Administration

Guillaume Brat

I am employed by NASA and I am the Technical Area Lead of the Robust Software Engineering (RSE) group in the Intelligent Systems Division at NASA Ames. The RSE group conducts research on new verification and validation techniques, mostly based on formal methods. I received an M.Sc. and Ph.D. from the ECE Department at The University of Texas at Austin.

I am also an SPM for the System-Wide Safety (SWS) project in the Airspace Operations and Safety program (AOSP) in ARMD. I am co-leading (with colleagues at Langley) two TCs focusing in assurance for aviation. TC 3 aims at making the assurance and certification process for traditional aviation systems (e.g., transport aircraft) more efficient while at least maintaining, if not increasing, the current level of safety. TC 4 focuses on assurance for autonomous systems, or more largely on emerging markets in aviation, and on proposing a certification process for it to the FAA..

As a researcher, I have worked mostly on static code 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, 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 assurance and certification 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 -