NASA Logo, National Aeronautics and Space Administration

Ewen Denney

Photo of Ewen Denney

Ewen Denney
Research Scientist
Robust Software Engineering Group












Biography

I'm a research scientist in the Robust Software Engineering Group of the Intelligent Systems Division at the NASA Ames Research Center in Mountain View, California. I am working on automated program synthesis and certification.

Research

Program synthesis is the automatic construction of correct and efficient executable code from high-level declarative specifications. I work 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 currently working on making the synthesis systems more extensible, by developing an appropriate notion of explicit model to represent the information used and generated during schema-based synthesis.

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).

My current research in this area is on extending the range of safety policies that our system can deal with, and significantly reducing the effort which is involved in getting the system to certify with new policies, schemas, and specifications. This is achieved by raising the level of abstraction at which the policies are described, and using AI-style techniques to infer the necessary annotations.

Publications

Contact

NASA Ames Research Center
Computational Sciences Division
Mail Stop 269-2
Moffett Field, CA 94035

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