|
Software Engineering
|
Contact Information
|
|
Arnaud Venet
I conduct research within the Robust Software Engineering Group in the Computational Sciences Division (Code IC) at the NASA Ames Research Center. I obtained an M.Sc. (“Magistère”) from Ecole Normale Supérieure (1995) and a Ph.D. from Ecole Polytechnique (1998) in France. I am employed via Kestrel Technology. My research focuses on making precise abstract interpretation techniques scale to large programs. The ultimate purpose of my work is to develop abstract interpretation algorithms that give useful information and are efficient enough to be shipped with production-level compilers. I am the architect and main developer of C Global Surveyor (CGS) a static array-bound checker based on Abstract Interpretation that is able to analyze C codes of several hundreds of KLOC in a couple of hours and solve over 80% of all pointer dereferences. CGS is based on a pointer analysis specialized for array-bound checking and uses distributed algorithms that allow the tool to run on a cluster of machines. A detailed description of the algorithms implemented in CGS can be found in [7]. CGS has been successfully applied to the flight control software of several Mars missions: Mars Path Finder (140 KLOC), Deep Space 1 (280 KLOC) and Mars Exploration Rovers (550 KLOC). Publications
[1] Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs Arnaud Venet 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. [2] Abstract Interpretation of the Pi-Calculus Arnaud Venet Analysis and Verification of Multiple-Agent Languages, 5th LOMAPS Workshop, Stockholm, Sweden. Lecture Notes in Computer Science, pages 51-75, volume 1192, Springer 1997. [3] Automatic Determination of Communication Topologies in Mobile Systems Arnaud Venet 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. [4] Automatic Analysis of Pointer Aliasing for Untyped Programs Arnaud Venet Science of Computer Programming, pages 223-248, volume 35(2), 1999. [5] Nonuniform Alias Analysis of Recursive Data Structures and Arrays Arnaud Venet 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. [6] Experimental Evaluation of Verification and Validation Tools on Martian Rover Software [7] Precise and Efficient Static Array Bound Checking for Large Embedded C Programs Arnaud Venet and
Proceedings of the International Conference on Programming Language Design and Implementation, PLDI’04,
Pages 231-242, ACM Press 2004. © ACM. See copyright notice on the first page of the paper.
[8] A Scalable Nonuniform Pointer Analysis for Embedded Programs Arnaud Venet Proceedings of the International Static Analysis Symposium, SAS 04, Verona, Italy. Lecture Notes in Computer Science, pages 149-164, volume 3148, Springer 2004. [9] Precise and Scalable Static Program Analysis of NASA Flight Software
To appear in the Proceedings of the 2005 IEEE Aerospace Conference, Big Sky, MT, USA. IEEE Press 2005. |
NASA Ames Research Center |
+ Freedom of Information Act
+ Budgets, Strategic Plans and Accountability Reports
+ The President's Management Agenda
+ NASA Privacy Statement, Disclaimer,
and Accessibility Certification
+ Inspector General Hotline
+ Equal Employment Opportunity Data Posted Pursuant
to the No Fear Act
+ Information-Dissemination Priorities and Inventories
NASA Official: Dave Korsmeyer
Curated By: Asani Solutions