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 '13, ASE '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 techniqes 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

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