NASA Logo, National Aeronautics and Space Administration

Arnaud Venet

I am a Research Scientist in the Robust Software Engineering Group of the Intelligent Systems Division at NASA Ames Research Center in Mountain View, California. I received a Ph.D. from École Polytechnique (France) and an M.Sc. from École Normale Supérieure (France).

My research area is static program analysis by Abstract Interpretation. With Guillaume Brat, we designed a static analyzer for C programs named C Global Surveyor (CGS). CGS has been applied to the flight software of several NASA missions such as Mars Path Finder, Deep Space 1 and Mars Exploration Rovers, as well as ISS payload software (UPA). CGS has been shown to scale to codes over 550K LOC.

My research work focuses on algorithms and techniques for specializing static analyzers in order to achieve high precision and performance on large codes. I have developed a static analyzer generator named CodeHawk that allows the rapid development of customized static analyzers. I am the architect of IKOS (Inference Kernel for Open Static analyzers), a high-performance static analysis platform based on Abstract Interpretation and developed at NASA. IKOS has been demonstrated to yield low false positive rates (< 5%) on embedded avionic code up to 270 KLOC, with analysis times ranging in minutes on a laptop.

Publications

  • Arnaud Venet. Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs. In Proceedings of the 3rd International Symposium on Static Analysis SAS’96, Aachen, Germany. Lecture Notes in Computer Science, pages 366-382, volume 1145, Springer 1996 (PDF).
  • Arnaud Venet. Abstract Interpretation of the Pi-Calculus. In Analysis and Verification of Multiple-Agent Languages, 5th LOMAPS Workshop, Stockholm, Sweden. Lecture Notes in Computer Science, pages 51-75, volume 1192, Springer 1997 (PDF).
  • Arnaud Venet. Automatic Determination of Communication Topologies in Mobile Systems. In Proceedings of the 5th International Symposium on Static Analysis, SAS ’98, Pisa, Italy. Lecture Notes in Computer Science, pages 152-167, volume 1503, Springer 1998 (PDF).
  • Arnaud Venet. Automatic Analysis of Pointer Aliasing for Untyped Programs. In Science of Computer Programming, pages 223-248, volume 35(2), 1999 (PDF).
  • Arnaud Venet. Nonuniform Alias Analysis of Recursive Data Structures and Arrays. In Proceedings of the 9th International Symposium on Static Analysis SAS’02, Madrid, Spain. Lecture Notes in Computer Science, pages 36-51, volume 2477, Springer 2002 (PDF).
  • Arnaud Venet, Guillaume Brat. Precise and Efficient Static Array Bound Checking for Large Embedded C Programs. In Proceedings of the International Conference on Programming Language Design and Implementation, PLDI’04, Washington DC, USA, pages 231-242 (PDF).
  • Arnaud Venet. A Scalable Nonuniform Pointer Analysis for Embedded Programs. In Proceedings of the International Static Analysis Symposium, SAS 04, Verona, Italy. Lecture Notes in Computer Science, pages 149-164, volume 3148, Springer 2004 (PDF).
  • Guillaume Brat and Arnaud Venet. Precise and Scalable Static Program Analysis of NASA Flight Software. In Proceedings of the IEEE Aerospace Conference, Big Sky, MT, March, 2005 (PDF).
  • Guillaume Brat, Doron Drusinsky, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Richard Washington, Willem Visser. Experimental Evaluation of Verification and Validation Tools on Martian Rover Software. In Formal Methods in Systems Design Journal, Volume 25, September 2005 (PDF).
  • S. Thompson, A. Mycroft, G. Brat and A. Venet. Automatic In-Flight Repair of FPGA Cosmic Ray Damage. In Proceedings of the 1st Disruption in Space Symposium, Marseille, July, 2005 (PDF).
  • Arnaud Venet. Towards the Integration of Symbolic and Numerical Static Analysis. In Proceedings of the Conference on Verified Software: Theories, Tools, Experiments, VSTTE’05, Zurich, 10-14 October 2005 (PDF).
  • John Anton, Eric Bush, Allen Goldberg, Klaus Havelund, Doug Smith, and Arnaud Venet. Towards the Industrial Scale Development of Custom Static Analyzers. In Proceedings of the NIST Static Analysis Summit, Gaithersburg, MD, USA 2006 (PDF).
  • Eric Féron and Arnaud Venet. Static Stability Analysis of Embedded, Autocoded Software. In Proceedings of the Workshop on Verified Software: Tools, Theories, Experiments, VSTTE’06, Seattle, 2006. Microsoft Research Report (PDF).
  • Arnaud Venet. Static Analysis for High Assurance and Security. NSA Conference on High Confidence Software and Systems, Linthicum Heights, MD, USA 2007.
  • Arnaud Venet. A Practical Approach to Formal Software Verification by Static Analysis. In Ada Letters XXVIII, 1 (Apr. 2008), 92-95 (PDF).
  • Sarah Thompson, Guillaume Brat and Arnaud Venet. Software Model Checking of ARINC-653 Flight Code with MCP. In Proceedings of the Second NASA Formal Methods Symposium, Washington D.C., USA 2010 (PDF).
  • Arnaud Venet and Michael Lowry. Static Analysis for Software Assurance: Soundness, Scalability and Adaptiveness. In Proceedings of the Workshop on the Future of Software Engineering Research (FoSER'2010), Santa Fe, NM, USA 2010, pages 393-396 (PDF).
  • Arnaud Venet. The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. In Proceedings of Computer Aided Verification (CAV 2012), Berkeley, California, USA 2012. Lecture Notes in Computer Science, pages 139-154, volume 7358, Springer 2012 (PDF).

Contact

Intelligent Systems Division
NASA Ames Research Center
Mail Stop 269-2
Bldg. 269, Rm. 234
P.O. Box 1
Moffett Field, CA 94035-0001
Phone: +1 650-604-1337
Fax: +1 650-604-4036

Email: arnaud.j.venet@nasa.gov

First Gov logo
NASA Logo - nasa.gov