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

Certifiable Synthesis
Extensible Program Synthesis
Theorem Proving
Older publications

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, 101K)]

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 of AI 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)]