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.
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
- Certifiable Synthesis
- Extensible Program Synthesis
- Theorem Proving
- Older publications (program refinement, program extraction, Java Card)
-
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)]
-
Ki Yung Ahn and Ewen Denney, "A Framework for Testing First-Order Logic Axioms in Program Verification",
Software Quality Journal, 2011. To appear.
[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, p 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".
InProceedings 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". InProceedings 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". InProceedings 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". InProceedings 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".
InProceedings of the ICALP Workshop on Structures
and Deductions, July 2005.
[papers (PDF, 161K), (Postscript, 252K)] -
Events I have chaired/will chair: ASE '13, GPCE '11, PCC '09, NFM '09, ASE 08 Tools Track,SoftCeMent '05Conferences
2011Automated Software Engineering (ASE '11). November 2011
Automated Theory Engineering Workshop
(ATE '11). July 201114th Brazilian Symposium on Formal Methods
(SBMF '11). September 2011IEEE Software Engineering Workshop
(SEW '11). June 2011Secure Software Integration and Reliability Improvement
(SSIRI '11). June 2011NASA Formal Methods Symposium
(NFM '11). April 2011Generative Programming and Component Engineering
(GPCE '11). October 2011
Chair
2010Secure Software Integration and Reliability Improvement
(SSIRI '10). June 2010NASA Formal Methods Symposium
(NFM '10). April 2010Generative Programming and Component Engineering
(GPCE '10). October 201013th Brazilian Symposium on Formal Methods
(SBMF '10). November 2010User Interfaces for Theorem Provers
(UITP '10). July 2010International Conference on Automated Software Engineering
(ASE '10). September 2010
2009IEEE/ACM International Conference on Automated Software Engineering. November 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.
2008Generative 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.
200714th 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.
2006User Interfaces for Theorem Provers (UITP '06). August 2006.
2005Software 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 Official: Dave Korsmeyer
- Curator: ASANI Solutions