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
-
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,
181K)]
-
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". InInternational 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".
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)]
-
Conferences
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
NASA Formal Methods. April 2009.
Organizer
ICSE Research Demos. May 2009.
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.
User Interfaces for Theorem Provers (UITP '08).
August 2008.
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.
User Interfaces for Theorem Provers (UITP '06).
August 2006.
Software
Certificate Management (SoftCeMent '05).
November 2005.
Organizer
Constructive
Logic for Robust Software Engineering (CLASE
'05). April 2005.