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 '14, ASE '13, ASSURE '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 techniques 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

<ul style="margin-left:0px; list-style-position:inside">
  • Ewen Denney, Dwight Naylor, and Ganesh Pai, "Querying Safety Cases", In 33rd International Conference on Computer Safety, Reliability and Security (SafeComp '14), Florence, Italy, September 2014.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "Automating the Assembly of Aviation Safety Cases", In IEEE Transactions on Reliability, PP(99):1-20, July 2014.
    [paper (PDF), IEEE Xplore]

  • David Aspinall, Ewen Denney, and Christoph Lüth, "A Semantic Basis for Proof Queries and Transformations", In 19th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Stellenbosch, South Africa, December 2013.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, " Evidence Arguments for Using Formal Methods in Software Certification", In IEEE International Workshop on Software Certification (WoSoCer 2013), November 2013.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "A Formal Basis for Safety Case Patterns", In Proceedings of the 32nd International Conference on Computer Safety, Reliability and Security (SafeComp '13), Toulouse, France, September 2013.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, Iain Whiteside, "Hierarchical Safety Cases", NASA Formal Methods Symposium, NASA Ames, CA, May 2013.
    [paper (PDF)]

  • Ewen Denney, Iain Whiteside, "Hierarchical Safety Cases", Technical Report NASA/TM-2012-216481, NASA Ames Research Center, December 2012.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, and Joe Pohl, "Automating the Generation of Heterogeneous Aviation Safety Cases", Technical Report NASA/CR-2011-215983, NASA Ames Research Center, August 2011.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, and Joe Pohl, "AdvoCATE: An Assurance Case Automation Toolset", Proceedings of the Workshop on Next Generation of System Assurance Approaches for Safety Critical Systems (SASSUR), Magdeburg, Germany, September 2012.
    [paper (PDF)]

  • Ewen Denney, Ganesh Pai, Corey Ippolito, and Ritchie Lee, "An Integrated Safety and Systems Engineering Methodology for Small Unmanned Aircraft Systems", Infotech@Aerospace, Garden Grove, CA, June 2012.
    [paper (PDF)]

  • Ewen Denney and Ganesh Pai, "A Lightweight Methodology for Safety Case Assembly", Proceedings of the 31st International Conference on Computer Safety, Reliability and Security (SafeComp '12), Magdeburg, Germany, September 2012.
    [paper (PDF)]

  • 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, pp 1-42, November 2011.
    [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)]

  •    <li>
            Ki Yung Ahn and Ewen Denney, <strong>"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, pp 309-330.
    [paper (PDF, 344K)]

  •     <li>
        Ewen Denney, Bernd Fischer, <strong>"A Verification-Driven Approach to Traceability and Documentation for Auto-Generated Mathematical Software,"</strong>
        <i>IEEE/ACM International Conference on Automated Software Engineering (ASE09)</i>,
         Auckland, New Zealand, Nov. 16th, 2009.
        <br>
         [paper (<strong><a href="/m/pub-archive/597/denney-fischer-ase09.pdf">PDF, 286K</a></strong>)]
        <br><br>
        </li>
        <li>
            Nurlida Basir, Ewen Denney, and Bernd Fischer, <strong>"Deriving 
            safety cases from automatically constructed proofs"
            </strong>. In <i>The 4th IET International Conference 
            on System Safety</i>. London, England, 
            Oct. 26, 2009.
            <br>
            [paper (<strong><a href="/m/pub-archive/729/Safety2009_0004_final.pdf">PDF, 357K</a></strong>)]<br><br>
        </li>
        <li>
            Ewen Denney, Bernd Fischer, <strong>"Generating code 
            review documentation for auto-generated mission-critical software."
            </strong>. In <i>Third IEEE International Conference on Space Mission
            Challenges for Information Technology (SMC-IT)</i>. Pasadena, CA, Jul. 19-23, 2009.
            <br>
            [paper (<strong><a href="/m/pub-archive/580/SMC-IT-Denney.pdf">PDF,
                    1.5M</a></strong>)]<br><br>
        </li>
    

  • 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</i>. Portland, Oregon,
            Oct. 22-26, 2006.
            <br>
            [paper (<strong><a href="/m/profile/edenney/papers/gpce06-denney.pdf">PDF,
                    166K</a></strong>)]<br><br>
        </li>
        <li>
            Ewen Denney, Bernd Fischer, <strong>"Annotation
                inference for the safety certification
                automatically generated code"</strong>. In <i>Proc.
                ASE '06: 21st IEEE/ACM International Conference on
                Automated Software Engineering</i>. Tokyo, Japan,
            Sep. 18-22, 2006.
            <br>
            [paper (<strong><a href="/m/profile/edenney/papers/ase06-denney.pdf">PDF,
                    63K</a></strong>)]<br><br>
        </li>
        <li>
            Guillaume Brat, Ewen Denney, Dimitra
            Giannakopoulou, Jeremy Frank, and Ari Jonsson.<b>"Verification of Autonomous Systems for Space
                Applications".</b>
            In <i>Proceedings of the IEEE
                Aerospace Conference</i>. Big Sky, MT, March
            2006.
            <br>
            [paper (<b><a href="/m/profile/edenney/papers/Autonomy_VnV.pdf">PDF, 323K</a></b>)]
            <br><br>
        </li>
        <li>
            Guillaume Brat, Ewen Denney, Kim Farell,
            Dimitra Giannakopoulou, Ari Jonsson, Jeremy Frank,
            Mark Boddy, Todd Carpenter, Tara Estlin, and Mihail 
            Pivtoraiko. <b>"A Robust Compositional Architecture
                for Autonomous Systems".</b>
            In <i>Proceedings of
                the IEEE Aerospace Conference</i>. Big Sky, MT,
            March 2006.
            <br>
            [paper (<b><a href="/m/profile/edenney/papers/Robust_Autonomous.pdf">PDF,
                    417K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney, Bernd Fischer and Johann Schumann.<b>"An Empirical Evaluation of Automated Theorem
                Provers in Software Certification"</b>. In <i>International Journal on Artificial Intelligence Tools</i>. Vol. 15,
            no. 1, pp. 81-107, Feb. 2006.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/ijait.pdf">PDF,
                    517K</a></b>), (<b><a href="/m/profile/edenney/papers/ijait.ps">Postscript, 6.8M</a></b>)]
            <br>
            Also appears in <i>Proceedings of the IJCAR 2004
                Workshop on Empirically Successful First Order
                Reasoning (ESFOR)</i>, July 2004, Cork,
            Ireland.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/esfor2004.pdf">PDF,
                    239K</a></b>), (<b><a href="/m/profile/edenney/papers/esfor2004.ps">Postscript,
                    525K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney and Bernd Fischer. <b>"A program
                certification assistant based on fully automated
                theorem provers"</b>. In <i>Proceedings of the
                International Workshop on User Interfaces for
                Theorem Provers, (UITP'05)</i>, April 2005, pp
            98-116.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/uitp05.pdf">PDF,
                    1.3M</a></b>), (<b><a href="/m/profile/edenney/papers/uitp05.ps">Postscript, 22M</a></b>)]
            <br><br>
        <li>
            Ewen Denney, Bernd Fischer, Dieter Hutter, and 
            Mark Jones. <b>"Proceedings of the 2005 ASE
                Workshop on Software Certificate Management".</b>
            Long Beach, CA, Nov. 8, 2005.
            <br>
            [proceedings (<b><a href="/m/project/sc05/papers/sc05-proceedings.pdf"> PDF, 1.8M</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney and Bernd Fischer. <b>"Software
                Certification and Software Certificate Management
                Systems".</b>
            In <i>Proceedings of 2005 ASE
                Workshop on Software Certificate Management</i>.
            Long Beach, CA, pp. 1-5, Nov. 2005.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/Denney-Fischer-softcement05.pdf">PDF,
                    35K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney and Bernd Fischer. <b>"Certifiable
                program generation".</b>
            In <i>Proceedings of
                Generative Programming and Component Engineering
                2005</i>. pages 17-28, Sep-Oct 2005, Lecture Notes
            in Computer Science 3676, Springer. Tallinn,
            Estonia 2005. Invited talk.
            <br>
            [paper (<b><a href="/m/profile/edenney/papers/gpce05.pdf">PDF,
                    106K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney and Bernd Fischer. <b>"Formal
                safety certification of aerospace software".</b>
            In<i>Proceedings of Infotech@Aerospace</i>. AIAA,
            September 2005. Invited talk.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/DenneyFischer-infotech.pdf">PDF,
                    427K</a></b>), (<b><a href="/m/profile/edenney/papers/DenneyFischer-infotech.ps">Postscript,
                    789K</a></b>)]
            <br><br>
        </li>
        <li>
            Geoff Sutcliffe, Ewen Denney, and Bernd 
            Fischer. <b>"Practical proof checking for program
                certification".</b>
            In <i>Proceedings of the
                CADE-20 Workshop on Empirically Successful
                Classical Automated Reasoning (ESCAR'05)</i>, July
            2005.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/escar05.pdf">PDF,
                    95K</a></b>), (<b><a href="/m/profile/edenney/papers/escar05.ps">Postscript,
                    103K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney, Bernd Fischer, Johann Schumann, 
            and Julian Richardson. <b>"Automatic certification
                of Kalman filters for reliable code
                generation"</b>. In <i>Proceedings of the IEEE
                Aerospace Conference</i>. Big Sky, Montana. IEEE,
            March 2005.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/aerocertification.pdf">PDF,
                    369K</a></b>), (<b><a href="/m/profile/edenney/papers/aerocertification.ps">Postscript,
                    5.5M</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney and Ram Prasad Venkatesan. <b>"A
                Generic Software Safety Document Generator"</b>. In<i>Proceedings of the 10th International Conference
                on Algebraic Methodology and Software Engineering
                (AMAST 2004)</i>. pp. 102-116, Stirling, Scotland,
            2004.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/DenneyAMAST04.pdf">PDF, 176K</a></b>),
            (<b><a href="/m/profile/edenney/papers/DenneyAMAST04.ps">Postscript,
                    213K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney, Bernd Fischer and Johann Schumann.<b>"Using Automated Theorem Provers to Certify
                Auto-Generated Aerospace Software"</b>. In<i>Proceedings of the 2nd International Joint
                Conference on Automated Reasoning (IJCAR'04)</i>,
            LNAI 3097, pp. 198-212, Cork, Ireland, 2004.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/cade2004.pdf">PDF,
                    162K</a></b>), (<b><a href="/m/profile/edenney/papers/cade2004.ps">Postscript,
                    204K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney, Bernd Fischer and Johann Schumann.<b>"Adding Assurance to Automatically Generated
                Code".</b>
            In <i>Proceedings of the 8th IEEE
                International Symposium on High Assurance Systems
                Engineering</i>
            (HASE 2004). Tampa, Florida, 25-26
            March 2004.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/DenneyHase2004.pdf">PDF, 51K</a></b>),
            (<b><a href="/m/profile/edenney/papers/DenneyHase2004.ps">Postscript,55K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney and Bernd Fischer. <b>"Correctness
                of Source-Level Safety Policies"</b>. In<i>Proceedings of the 12th International FME
                Symposium</i>. Pisa, Italy, 8-14 September 2003.
            LNCS Volume 2805, pp. 894-913.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/fm03.pdf">PDF,
                    234K</a></b>), (<b><a href="/m/profile/edenney/papers/fm03.ps">Postscript, 285K</a></b>)]
            <br><br>
            <a name= "Extensible%20Program%20Synthesis"></a>
        </li>
        <li>
            Tomas Bures, Ewen Denney, Bernd Fischer, and 
            Eugen C. Nistor. <b>"The role of ontologies in
                schema-based program synthesis"</b>. In <i>Workshop
                on Ontologies as Software Engineering
                Artifacts</i>, Vancouver, Canada, 2004.
        </li>
        <li style="list-style: none">
            [papers (<b><a href="/m/profile/edenney/papers/ontologies.pdf">PDF, 69K</a></b>), (<b><a href="/m/profile/edenney/papers/ontologies.ps">Postscript,
                    97K</a></b>)]
            <br>
            <br>
        </li>
        <li>
            Ewen Denney, Jon Whittle. <b>"Combining
                Model-driven and Schema based Program
                Synthesis"</b>. In <i>Proceedings of the 1st
                International Conference on the Applications of UML
                and MDA to Software Systems</i>
            (UMSS'2004), June
            21-24, 2004, Las Vegas, Nevada.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/umss04.pdf">PDF,
                    117K</a></b>), (<b><a href="/m/profile/edenney/papers/umss04.ps">Postscript, 174K</a></b>)]
            <br><a name="Theorem%20Proving"></a><br>
        </li>
        <li>
            Ewen Denney, John Power, and Konstantinos 
            Tourlas. <b>"Hiproofs: A hierarchical notion of
                proof tree"</b>. In <i>Proceedings of the 21st
                Annual Conference on Mathematical Foundations of
                Programing Semantics (MFPS XXI), 2005</i>, volume
            155 of Electronic Notes in Theoretical Computer
            Science (ENTCS), pp. 341-359. Elsevier Science
            Direct, May 2006.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/mfps05.pdf">PDF,
                    351K</a></b>), (<b><a href="/m/profile/edenney/papers/mfps05.ps">Postscript, 407K</a></b>)]
            <br><br>
        </li>
        <li>
            Ewen Denney, John Power, and Konstantinos 
            Tourlas. <b>"Hierarchical proof structures".</b>
            In<i>Proceedings of the ICALP Workshop on Structures
                and Deductions</i>, July 2005.
            <br>
            [papers (<b><a href="/m/profile/edenney/papers/sd05.pdf">PDF,
                    161K</a></b>), (<b><a href="/m/profile/edenney/papers/sd05.ps">Postscript, 252K</a></b>)]
        </li>
        <li style="list-style: none">
            <br>
            <br>
    
            <h3>Conferences</h3>
    


    2014

    17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014). April 2014

    Sixth NASA Formal Methods Symposium (NFM 2014). April-May 2014

    19th International Symposium on Formal Methods - Industry Track (FM 2014). May 2014

    ICSE Software Engineering In Practice (SEIP) Track (SEIP 2014). May-June 2014

    8th International Conference on Software Security and Reliability (SERE' 14). June-July 2014

    17th Brazilian Symposium on Formal Methods (SBMF) (SBMF 2014). September-October 2014


    2013

    Fundamental Approaches to Software Engineering
    (FASE '13). March 2013

    NASA Formal Methods 2013
    (NFM '13). May 2013

    Assurance Cases for Software-intensive Systems
    (ASSURE '13). May 2013

    Proof Exchange for Theorem Proving
    (PxTP '13). June 2013

    7th International Conference on Software Security and Reliability (SERE '13). June 2013

    32nd International Conference on Computer Safety, Reliability and Security
    (SafeComp '13). September 2013

    28th IEEE/ACM International Conference on Automated Software Engineering (ASE '13). November 2013

    Brazilian Symposium on Formal Methods (SBMF) (SBMF 2013). September-October 2013

    1st International Workshop on Argument for Agreement and Assurance (AAA '13). October 2013

    3rd International Workshop on Open Systems Dependability (WOSD 2013). November 2013


    2012

    NASA Formal Methods Symposium
    (NFM '12). April 2012

    Software Security and Reliability (SERE '12). June 2012

    
    

    Interactive Theorem Proving
    (ITP '12). August 2012

    Automated Software Engineering (ASE '12). September 2012

    15th Brazilian Symposium on Formal Methods
    (SBMF '12). September 2012

    IEEE Software Engineering Workshop
    (SEW-35). October 2012

    Workshop on Open Systems Dependability
    (WOSD '12). November 2012


    2011

    Automated Software Engineering (ASE '11). November 2011

    Automated Theory Engineering Workshop
    (ATE '11). July 2011

    14th Brazilian Symposium on Formal Methods
    (SBMF '11). September 2011

    IEEE Software Engineering Workshop
    (SEW '11). June 2011

    Secure Software Integration and Reliability Improvement
    (SSIRI '11). June 2011

    
    

    NASA Formal Methods Symposium
    (NFM '11). April 2011


    Generative Programming and Component Engineering
    (GPCE '11). October 2011

    Chair


    2010

    Secure Software Integration and Reliability Improvement
    (SSIRI '10). June 2010

    <p>
                <b><a target="_blank" href="http://shemesh.larc.nasa.gov/NFM2010/">NASA Formal Methods Symposium<br> (NFM '10). April 2010 </a></b>
            </p>
    
    <p>
                <b><a target="_blank" href="http://www.resource-aware.org/do/view/GPCE10/">Generative Programming and Component Engineering<br>(GPCE '10). October 2010</a></b>
            </p>
    

    13th Brazilian Symposium on Formal Methods
    (SBMF '10). November 2010

    User Interfaces for Theorem Provers
    (UITP '10). July 2010

    International Conference on Automated Software Engineering
    (ASE '10). September 2010

          <p>
                <b><a target="_blank" href="http://soft.vub.ac.be/ase2010/calls#call_for_tool_demonstrations">ASE Tools Track 2010</a></b>
            </p>
    


    2009

            <p>
                <b><a target="_blank" href="https://www.se.auckland.ac.nz/conferences/ase09/">IEEE/ACM International Conference on Automated Software Engineering. November  2009.</a></b>
            </p>
    

    ASE Tools Track 2009

            <p>
                <b><a target="_blank" href="http://sbmf2009.inf.ufrgs.br">SBMF (Brazilian Formal Methods) 2009</a></b>
            </p>
            <p>
                <b><a target="_blank" href="/events/pcc09/">3rd International Workshop on Proof Carrying Code and Software Certification. August 2009 </a></b>
    


    Organizer, Chair

    NASA Formal Methods. April 2009.
    Organizer, Chair

    ICSE Research Demos. May 2009.


    2008

            <p>
                <b>Generative Programming and Component Engineering. October 2008.</b>
            </p>
            <p>
                <b><a target="_blank" href="http://www.lasid.ufba.br/sbmf2008/">11th
                        Brazilian Symposium on Formal Methods. August
                        2008.</a></b>
            </p>
            <p>
                <b><a target="_blank" href="http://workshops.inf.ed.ac.uk/pcc08/">2nd
                        International Workshop on Proof-Carrying Code
                        (PCC '08). June 2008.</a></b>
            </p>
            <p>
                <b>15th
                        Asia-Pacific Software Engineering Conference
                        (APSEC '08). December 2008.</b>
            </p>
            <p>
                <b><a target="_blank" href="http://www.di.univaq.it/ase2008/">Automated
                        Software Engineering (ASE '08). September
                        2008.</a></b>
    


    Chair

    User Interfaces for Theorem Provers (UITP '08). August 2008.


    2007

            <p>
                <b><a target="_blank" href="http://apsec2007.fuka.info.waseda.ac.jp/">14th
                        Asia-Pacific Software Engineering Conference
                        (APSEC '07). December 2007.</a></b>
            </p>
            <p>
                <b><a target="_blank" href="http://www.cse.msu.edu/ase2007/">Automated
                        Software Engineering (ASE '07). November
                        2007.</a></b>
            </p>
            <p>
                <b><a target="_blank" href="http://www.sbmf2007.ufop.br/">10th Brazilian
                        Symposium on Formal Methods. August
                        2007.</a></b>
            </p>
            <p>
                <b>12th IEEE International Conference on
                        Engineering of Complex Computer Systems (ICECCS
                        '07). July 2007.</b>
            </p>
            <p>
                <b><a target="_blank" href="http://www.risc.uni-linz.ac.at/about/conferences/WING2007/index.html">1st International Workshop on Invariant
                        Generation (WING '07). June 2007.</a></b>
            </p>
    


    2006

            <p>
                <b><a target="_blank" href="http://www.ags.uni-sb.de/~omega/workshops/UITP06/">User Interfaces for Theorem Provers (UITP '06).
    
                        August 2006.</a></b>
            </p>
    


    2005

            <p>
                <b>Software
                        Certificate Management (SoftCeMent '05).
                        November 2005.</b>
                <br>
                Organizer, Chair
                <br>
            </p>
            <p>
                <b><a target="_blank" href="http://www.csse.monash.edu.au/clase/">Constructive
                        Logic for Robust Software Engineering (CLASE
                        '05). April 2005.</a></b>
            </p>
    
    
    
        </li>
    </ul>
    
  • 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