NASA Logo, National Aeronautics and Space Administration

Ewen Denney

Photo of Ewen Denney

Ewen Denney
Senior Computer Scientist
Robust Software Engineering Group












Biography

I'm a computer scientist in the Robust Software Engineering Group of the Intelligent Systems Division at the NASA Ames Research Center in Mountain View, California. I am developing safety assurance and certification methods based on automated program synthesis, verification using annotation inference and theorem provers, and the automated generation of safety cases.

Events I have chaired/will chair: ASSURE '14, ASE '13, ASSURE '13, ASE '12 Tools Track, GPCE '11, PCC '09, NFM '09, ASE '08 Tools Track,SoftCeMent '05

Summer Interns

Please get in touch if you are interested in summer internships working on topics related to the research described here.

Program Synthesis

Program synthesis is the automatic construction of correct and efficient executable code from high-level declarative specifications. I have worked on the AutoBayes and AutoFilter projects in the RSE group at NASA Ames, developing this technology primarily for application in the domains of statistical data analysis and state estimation.

I am also interested in correctness issues, specifically regarding the formal certification of synthesized code. Since synthesis systems are extremely complex, we don't want the correctness of the generated code to depend on the correctness of the generators (the correct-by-construction paradigm). Rather, the idea behind certifiable program synthesis is to generate code together with logical annotations which can then be used to produce verification conditions that are proved by an automated theorem prover. We have been pursuing an approach to certifying that the generated code satisfies one or more safety policies, such as memory safety; i.e., that each access to an array is within the bounds of the array (a general language-specific policy) or that certain vector terms have the appropriate norm (a domain-specific policy for the data analysis domain).

Verification

Based on work that started in certifiable program synthesis, we are developing the AutoCert tool to raise the level of abstraction at which the policies are described, and using AI-style techniques to infer the necessary annotations. AutoCert compiles domain-specific information into annotation patterns which can be used to verify requirements. It generates detailed safety reports that explain why the code meets its requirements, and traces between requirements, assumptions, and code.

Safety Cases

We can use AutoCert to generate fragments of safety cases. In an ongoing project, we are developing techniques to combine such formally generated safety case fragments with other, expert provided, material, in order to assemble full safety cases automatically.

Testing

Program verification systems based on automated theorem provers rely on user-provided axioms in order to verify domain-specific properties of code. However, formulating axioms correctly is nontrivial in practice. We adopt the idea of model-based testing to test axioms and thus qualify domain theories.

Publications

  • Ewen Denney, Ganesh Pai, and Iain Whiteside, "Model-driven Development of Safety Architectures", In Proceedings of the ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2017), Austin, TX, September 2017.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, and Iain Whiteside, "Modeling the Safety Architecture of UAS Flight Operations", In Proceedings of the 36th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2017), Trento, Italy, September 2017.
    [paper (PDF)]

  • Reece Clothier, Ewen Denney, and Ganesh Pai, "Making a Risk Informed Safety Case for Small Unmanned Aircraft System Operations", In Proceedings of the 17th AIAA Aviation Technology, Integration, and Operations Conference (ATIO 2017), Denver, CO, June 2017.
    [paper (PDF)]

  • Kyle White, Ewen Denney, Matt Knudson, Angelos Marnerides, and Dimitrios Pezaros, "A Programmable SDN+NFV-based Architecture for UAV Telemetry Monitoring", In Proceedings of the IEEE Consumer Communications and Networking Conference 2017, Las Vegas, NV, January 2017.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "Composition of Safety Argument Patterns", In Proceedings of the 35th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2016), Trondheim, Norway, September 2016.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "Safety Considerations for UAS Ground-based Detect and Avoid", In Proceedings of the 35th IEEE/AIAA Digital Avionics Systems Conference (DASC), Sacramento, CA, September 2016.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "Architecting a Safety Case for UAS Flight Operations", In Proceedings of the 34th International System Safety Conference (ISSC), Orlando, FL, August 2016.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "Towards a Formal Basis for Modular Safety Cases", In Proceedings of the 34th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2015), Delft, Netherlands, September 2015.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "Argument-based Airworthiness Assurance of Small UAS", In Proceedings of the 34th IEEE/AIAA Digital Avionics Systems Conference (DASC), Prague, Czech Republic, September 2015.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "A Methodology for the Development of Assurance Arguments for Unmanned Aircraft Systems", In Proceedings of the 33rd International System Safety Conference (ISSC), San Diego, CA, August 2015.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, "Safety Case Patterns: Theory and Applications", Technical Report NASA/TM-2015-218492, NASA Ames Research Center, February 2015.
    [paper (PDF)]

  • Ewen Denney, Ibrahim Habli, and Ganesh Pai, "Dynamic Safety Cases for Through-life Safety Assurance", In Proceedings of the 37th International Conference on Software Engineering (ICSE 2015), New Ideas and Emerging Results track (NIER), Florence, Italy, May 2015.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, and Iain Whiteside, "Formal Foundations for Hierarchical Safety Cases", In Proceedings of the 16th IEEE International Symposium on High Assurance Systems Engineering (HASE 2015), Daytona Beach, FL, January 2015.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, Randall Berthold, Matthew Fladeland, Bruce Storms, and Mark Sumich, "Assuring Ground-based Detect and Avoid for UAS Operations", In Proceedings of the 33rd Digital Avionics Systems Conference (DASC), Colorado Springs, CO, October 2014.
    [paper (PDF)]

  • Ewen Denney, Dwight Naylor, and Ganesh Pai, "Querying Safety Cases", In 33rd International Conference on Computer Safety, Reliability and Security (SafeComp '14), Florence, Italy, September 2014.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "Automating the Assembly of Aviation Safety Cases", In IEEE Transactions on Reliability, PP(99):1-20, July 2014.
    [paper (PDF), IEEE Xplore]

  • David Aspinall, Ewen Denney, and Christoph Lüth, "A Semantic Basis for Proof Queries and Transformations", In 19th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Stellenbosch, South Africa, December 2013.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, " Evidence Arguments for Using Formal Methods in Software Certification", In IEEE International Workshop on Software Certification (WoSoCer 2013), November 2013.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "A Formal Basis for Safety Case Patterns", In Proceedings of the 32nd International Conference on Computer Safety, Reliability and Security (SafeComp '13), Toulouse, France, September 2013.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, Iain Whiteside, "Hierarchical Safety Cases", NASA Formal Methods Symposium, NASA Ames, CA, May 2013.
    [paper (PDF)]

  • Ewen Denney, Iain Whiteside, "Hierarchical Safety Cases", Technical Report NASA/TM-2012-216481, NASA Ames Research Center, December 2012.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, and Joe Pohl, "Automating the Generation of Heterogeneous Aviation Safety Cases", Technical Report NASA/CR-2011-215983, NASA Ames Research Center, August 2011.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, and Joe Pohl, "AdvoCATE: An Assurance Case Automation Toolset", Proceedings of the Workshop on Next Generation of System Assurance Approaches for Safety Critical Systems (SASSUR), Magdeburg, Germany, September 2012.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, Corey Ippolito, and Ritchie Lee, "An Integrated Safety and Systems Engineering Methodology for Small Unmanned Aircraft Systems", Infotech@Aerospace, Garden Grove, CA, June 2012.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "A Lightweight Methodology for Safety Case Assembly", Proceedings of the 31st International Conference on Computer Safety, Reliability and Security (SafeComp '12), Magdeburg, Germany, September 2012.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, and Josef Pohl, "Heterogeneous Aviation Safety Cases: Integrating the Formal and the Non-formal", Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012), Paris, France, July 2012.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, and Ibrahim Habli, "Perspectives on Software Safety Case Development for Unmanned Aircraft", Proceedings of the 42nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2012), Boston, MA, June 2012.
    [paper (PDF)]

  • David Aspinall, Ewen Denney, and Christoph Lüth, "Querying Proofs", 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2012), Mérida, Venezuela, March 2012.
    [paper (PDF)]

  • Ewen Denney, Ibrahim Habli, and Ganesh Pai, "Towards Measurement of Confidence in Safety Cases", Proceedings of the 5th International Symposium on Empirical Software Engineering and Measurement (ESEM '11), Banff, Canada, September 2011.
    [paper (PDF)]

  • David Aspinall, Ewen Denney and Christoph Lüth, "Querying Proofs (Work in Progress)", Conference on Intelligent Computer Mathematics (CICM '11), Bertinoro, Italy, July 2011.
    [paper (PDF)]

  • Nurlida Basir, Ewen Denney and Bernd Fischer, "Building heterogeneous safety cases for automatically generated code", Infotech@Aerospace (Infotech '11), St Louis, MO, March 2011.
    [paper (PDF)]

  • Nurlida Basir, Ewen Denney and Bernd Fischer, "Deriving Safety Cases for Hierarchical Structure in Model-based Development," 29th International Conference on Computer Safety, Reliability and Security (SAFECOMP '10), Vienna, Austria, September 2010.
    [paper (PDF)]

  • Ki Yung Ahn and Ewen Denney, "Testing First-Order Logic Axioms in Program Verification," 4th International Conference on Tests & Proofs (TAP 2010), Malaga, Spain, July 1 2010 .
    [paper (PDF, 425K)]

  • David Aspinall, Ewen Denney, and Christoph Lüth, "Tactics for Hierarchical Proof". In Mathematics in Computer Science: Special Issue on Authoring, Digitalization and Management of Mathematical Knowledge, Vol. 3, No. 3, May 2010, pp 309-330.
    [paper (PDF, 344K)]

  • Ewen Denney, Bernd Fischer, "A Verification-Driven Approach to Traceability and Documentation for Auto-Generated Mathematical Software," IEEE/ACM International Conference on Automated Software Engineering (ASE09), Auckland, New Zealand, Nov. 16th, 2009.
    [paper (PDF, 286K)]

  • Nurlida Basir, Ewen Denney, and Bernd Fischer, "Deriving safety cases from automatically constructed proofs" . In The 4th IET International Conference on System Safety. London, England, Oct. 26, 2009.
    [paper (PDF, 357K)]

  • Ewen Denney, Bernd Fischer, "Generating code review documentation for auto-generated mission-critical software." . In Third IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT). Pasadena, CA, Jul. 19-23, 2009.
    [paper (PDF, 1.5M)]

  • Ewen Denney, Bernd Fischer, "Generating Customized Verifiers for Automatically Generated Code". In Proc. GPCE '08: 7th International Conference on Generative Programming and Component Engineering. Nashville, Tennessee , Oct. 19-23, 2008.
    [paper (PDF, 175K)]

  • Nurlida Basir, Ewen Denney, Bernd Fischer,"Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information". In The 27th International Conference on Computer Safety, Reliability and Security (SAFECOMP '08). Newcastle, England, September 2008.
    [paper (PDF, 162K)]

  • David Aspinall, Ewen Denney, and Christoph Lüth, "A Tactic Language for Hiproofs". In 7th International Conference on Mathematical Knowledge Management (MKM '08). Birmingham, England, July 2008.
    [paper (PDF, 290K)]

  • Ewen Denney, Bernd Fischer, "Explaining Verification Conditions". In 12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008). Urbana, Illinois, July 2008.
    [paper (PDF, 151K)]

  • Nurlida Basir, Ewen Denney, Bernd Fischer,"Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code". In International Workshop on the Certification of Safety-Critical Software Controlled Systems (SafeCert '08). Budapest, Hungary, March 2008.
    [paper (PDF, 218k)]

  • Ewen Denney, Steven Trac, "A Software Safety Certification Tool for Automatically Generated Guidance, Navigation and Control Code". In IEEE Aerospace Conference. Big Sky, MT, March 2008.
    [paper (PDF, 404K)]

  • Ewen Denney, Bernd Fischer, "Extending Source Code Generators for Evidence-based Software Certification". In 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA '06). Paphos, Cyprus, November 2006.
    [paper (PDF, 418K)]

  • Ewen Denney, Bernd Fischer, "A generic annotation inference algorithm for the safety certification of automatically generated code". In Proc. GPCE '06: 5th International Conference on Generative Programming and Component Engineering. Portland, Oregon, Oct. 22-26, 2006.
    [paper (PDF, 166K)]

  • Ewen Denney, Bernd Fischer, "Annotation inference for the safety certification automatically generated code". In Proc. ASE '06: 21st IEEE/ACM International Conference on Automated Software Engineering. Tokyo, Japan, Sep. 18-22, 2006.
    [paper (PDF, 63K)]

  • Guillaume Brat, Ewen Denney, Dimitra Giannakopoulou, Jeremy Frank, and Ari Jonsson."Verification of Autonomous Systems for Space Applications". In Proceedings of the IEEE Aerospace Conference. Big Sky, MT, March 2006.
    [paper (PDF, 323K)]

  • Guillaume Brat, Ewen Denney, Kim Farell, Dimitra Giannakopoulou, Ari Jonsson, Jeremy Frank, Mark Boddy, Todd Carpenter, Tara Estlin, and Mihail Pivtoraiko. "A Robust Compositional Architecture for Autonomous Systems". In Proceedings of the IEEE Aerospace Conference. Big Sky, MT, March 2006.
    [paper (PDF, 417K)]

  • Ewen Denney, Bernd Fischer and Johann Schumann."An Empirical Evaluation of Automated Theorem Provers in Software Certification". In International Journal on Artificial Intelligence Tools. Vol. 15, no. 1, pp. 81-107, Feb. 2006.
    [papers (PDF, 517K), (Postscript, 6.8M)]
    Also appears in Proceedings of the IJCAR 2004 Workshop on Empirically Successful First Order Reasoning (ESFOR), July 2004, Cork, Ireland.
    [papers (PDF, 239K), (Postscript, 525K)]

  • Ewen Denney and Bernd Fischer. "A program certification assistant based on fully automated theorem provers". In Proceedings of the International Workshop on User Interfaces for Theorem Provers, (UITP'05), April 2005, pp 98-116.
    [papers (PDF, 1.3M), (Postscript, 22M)]

  • Ewen Denney, Bernd Fischer, Dieter Hutter, and Mark Jones. "Proceedings of the 2005 ASE Workshop on Software Certificate Management". Long Beach, CA, Nov. 8, 2005.
    [proceedings ( PDF, 1.8M)]

  • Ewen Denney and Bernd Fischer. "Software Certification and Software Certificate Management Systems". In Proceedings of 2005 ASE Workshop on Software Certificate Management. Long Beach, CA, pp. 1-5, Nov. 2005.
    [papers (PDF, 35K)]

  • Ewen Denney and Bernd Fischer. "Certifiable program generation". In Proceedings of Generative Programming and Component Engineering 2005. pages 17-28, Sep-Oct 2005, Lecture Notes in Computer Science 3676, Springer. Tallinn, Estonia 2005. Invited talk.
    [paper (PDF, 106K)]

  • Ewen Denney and Bernd Fischer. "Formal safety certification of aerospace software". In Proceedings of Infotech@Aerospace. AIAA, September 2005. Invited talk.
    [papers (PDF, 427K), (Postscript, 789K)]

  • Geoff Sutcliffe, Ewen Denney, and Bernd Fischer. "Practical proof checking for program certification". In Proceedings of the CADE-20 Workshop on Empirically Successful Classical Automated Reasoning (ESCAR'05), July 2005.
    [papers (PDF, 95K), (Postscript, 103K)]

  • Ewen Denney, Bernd Fischer, Johann Schumann, and Julian Richardson. "Automatic certification of Kalman filters for reliable code generation". In Proceedings of the IEEE Aerospace Conference. Big Sky, Montana. IEEE, March 2005.
    [papers (PDF, 369K), (Postscript, 5.5M)]

  • Ewen Denney and Ram Prasad Venkatesan. "A Generic Software Safety Document Generator". In Proceedings of the 10th International Conference on Algebraic Methodology and Software Engineering (AMAST 2004). pp. 102-116, Stirling, Scotland, 2004.
    [papers (PDF, 176K), (Postscript, 213K)]

  • Ewen Denney, Bernd Fischer and Johann Schumann."Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software". In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04), LNAI 3097, pp. 198-212, Cork, Ireland, 2004.
    [papers (PDF, 162K), (Postscript, 204K)]

  • Ewen Denney, Bernd Fischer and Johann Schumann."Adding Assurance to Automatically Generated Code". In Proceedings of the 8th IEEE International Symposium on High Assurance Systems Engineering (HASE 2004). Tampa, Florida, 25-26 March 2004.
    [papers (PDF, 51K), (Postscript,55K)]

  • Ewen Denney and Bernd Fischer. "Correctness of Source-Level Safety Policies". In Proceedings of the 12th International FME Symposium. Pisa, Italy, 8-14 September 2003. LNCS Volume 2805, pp. 894-913.
    [papers (PDF, 234K), (Postscript, 285K)]

  • Tomas Bures, Ewen Denney, Bernd Fischer, and Eugen C. Nistor. "The role of ontologies in schema-based program synthesis". In Workshop on Ontologies as Software Engineering Artifacts, Vancouver, Canada, 2004.
  • [papers (PDF, 69K), (Postscript, 97K)]

  • Ewen Denney, Jon Whittle. "Combining Model-driven and Schema based Program Synthesis". In Proceedings of the 1st International Conference on the Applications of UML and MDA to Software Systems (UMSS'2004), June 21-24, 2004, Las Vegas, Nevada.
    [papers (PDF, 117K), (Postscript, 174K)]

  • Ewen Denney, John Power, and Konstantinos Tourlas. "Hiproofs: A hierarchical notion of proof tree". In Proceedings of the 21st Annual Conference on Mathematical Foundations of Programing Semantics (MFPS XXI), 2005, volume 155 of Electronic Notes in Theoretical Computer Science (ENTCS), pp. 341-359. Elsevier Science Direct, May 2006.
    [papers (PDF, 351K), (Postscript, 407K)]

  • Ewen Denney, John Power, and Konstantinos Tourlas. "Hierarchical proof structures". In Proceedings of the ICALP Workshop on Structures and Deductions, July 2005.
    [papers (PDF, 161K), (Postscript, 252K)]


  • Conferences


    2014

    17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014). April 2014

    Sixth NASA Formal Methods Symposium (NFM 2014). April-May 2014

    19th International Symposium on Formal Methods - Industry Track (FM 2014). May 2014

    ICSE Software Engineering In Practice (SEIP) Track (SEIP 2014). May-June 2014

    8th International Conference on Software Security and Reliability (SERE' 14). June-July 2014

    17th Brazilian Symposium on Formal Methods (SBMF) (SBMF 2014). September-October 2014


    2013

    Fundamental Approaches to Software Engineering
    (FASE '13). March 2013

    NASA Formal Methods 2013
    (NFM '13). May 2013

    Assurance Cases for Software-intensive Systems
    (ASSURE '13). May 2013

    Proof Exchange for Theorem Proving
    (PxTP '13). June 2013

    7th International Conference on Software Security and Reliability (SERE '13). June 2013

    32nd International Conference on Computer Safety, Reliability and Security
    (SafeComp '13). September 2013

    28th IEEE/ACM International Conference on Automated Software Engineering (ASE '13). November 2013

    Brazilian Symposium on Formal Methods (SBMF) (SBMF 2013). September-October 2013

    1st International Workshop on Argument for Agreement and Assurance (AAA '13). October 2013

    3rd International Workshop on Open Systems Dependability (WOSD 2013). November 2013


    2012

    NASA Formal Methods Symposium
    (NFM '12). April 2012

    Software Security and Reliability (SERE '12). June 2012

    Interactive Theorem Proving
    (ITP '12). August 2012

    Automated Software Engineering (ASE '12). September 2012

    15th Brazilian Symposium on Formal Methods
    (SBMF '12). September 2012

    IEEE Software Engineering Workshop
    (SEW-35). October 2012

    Workshop on Open Systems Dependability
    (WOSD '12). November 2012


    2011

    Automated Software Engineering (ASE '11). November 2011

    Automated Theory Engineering Workshop
    (ATE '11). July 2011

    14th Brazilian Symposium on Formal Methods
    (SBMF '11). September 2011

    IEEE Software Engineering Workshop
    (SEW '11). June 2011

    Secure Software Integration and Reliability Improvement
    (SSIRI '11). June 2011

    NASA Formal Methods Symposium
    (NFM '11). April 2011

    Generative Programming and Component Engineering
    (GPCE '11). October 2011

    Chair


    2010

    Secure Software Integration and Reliability Improvement
    (SSIRI '10). June 2010

    NASA Formal Methods Symposium
    (NFM '10). April 2010

    Generative Programming and Component Engineering
    (GPCE '10). October 2010

    13th Brazilian Symposium on Formal Methods
    (SBMF '10). November 2010

    User Interfaces for Theorem Provers
    (UITP '10). July 2010

    International Conference on Automated Software Engineering
    (ASE '10). September 2010

    ASE Tools Track 2010


    2009

    IEEE/ACM International Conference on Automated Software Engineering. November 2009.

    ASE Tools Track 2009

    SBMF (Brazilian Formal Methods) 2009

    3rd International Workshop on Proof Carrying Code and Software Certification. August 2009
    Organizer, Chair

    NASA Formal Methods. April 2009.
    Organizer, Chair

    ICSE Research Demos. May 2009.


    2008

    Generative Programming and Component Engineering. October 2008.

    11th Brazilian Symposium on Formal Methods. August 2008.

    2nd International Workshop on Proof-Carrying Code (PCC '08). June 2008.

    15th Asia-Pacific Software Engineering Conference (APSEC '08). December 2008.

    Automated Software Engineering (ASE '08). September 2008.
    Chair

    User Interfaces for Theorem Provers (UITP '08). August 2008.


    2007

    14th Asia-Pacific Software Engineering Conference (APSEC '07). December 2007.

    Automated Software Engineering (ASE '07). November 2007.

    10th Brazilian Symposium on Formal Methods. August 2007.

    12th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS '07). July 2007.

    1st International Workshop on Invariant Generation (WING '07). June 2007.


    2006

    User Interfaces for Theorem Provers (UITP '06). August 2006.


    2005

    Software Certificate Management (SoftCeMent '05). November 2005.
    Organizer, Chair

    Constructive Logic for Robust Software Engineering (CLASE '05). April 2005.

Contact

NASA Ames Research Center
Computational Sciences Division
Ewen Denney, Mail Stop 269-2
Bldg. 269, Rm. 234
P.O. Box 1
Moffett Field, CA 94035-0001

Phone: +1 (650) 604-2274
Ewen.W.Denney@nasa.gov

Links

+ NASA Ames
+ TI Home Page
+ RSE Homepage
+ NASA Home Page

First Gov logo
NASA Logo - nasa.gov