Skip Navigation
About NASALatest NewsMultimediaMissionsMy NASAWork For NASA

Publications :: Synthesis

Extensible Program Synthesis

Ewen Denney, Jon Whittle, "Combining Model-driven and Schema based Program Synthesis," Proc. UMSS'2004: 1st Int'l Conf. on the Applications of UML and MDA to Software Systems, Las Vegas, NV, pp. 207-211, Jun. 21-24, 2004.
[papers ( PDF, 117K), ( Postscript, 174K)]

Back to Top

AutoBayes: Synthesis of Data Analysis Software

Karen Gundy-Burlet, Johann Schumann, Tim Menzies, and Tony Barrett, "Parametric Analysis of Antares Re-Entry Guidance Algorithms using Advanced Test Generation and Data Analysis," Proc. i-SAIRAS'08: 9th International Symposium on Artificial Intelligence, Robotics, and Automation in Space , Universal City, California, February 25-29, 2008.
[paper (PDF, 451K)]

Bernd Fischer, Johann Schumann, Karen Huyser, Kevin Knuth, Domhnull Granquist-Fraser, Arsen Hajian, "Discovering Planetary Nebula Geometries: Explorations with a Hierarchy of Models," Proc. MAXENT'04: 24th Int'l Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, Munich, Germany, pp. 135-142, Jul. 25-30, 2004.
[papers (PDF, 386K )]

Bernd Fischer, Johann Schumann, "Applying AutoBayes to the Analysis of Planetary Nebulae Images (Extended Abstract)," Proc. ASE 2003: 18th IEEE Conf. on Automated Software Engineering, Montreal, Canada, pp. 337-342, Oct. 6-10, 2003.
[paper ( PDF, 153K)]

Bernd Fischer, Johann Schumann, "AutoBayes: A System for Generating Data Analysis Programs from Statistical Models," Journal of Functional Programming vol. 13, no. 3, pp. 483-508, May 2003.
[papers ( PDF, 398K), ( Postscript, 677K)]

Bernd Fisher, Johann Schumann, "Automated Synthesis of Statistical Data Analysis Programs," Proc. SDP'02: Workshop Science Data Processing, Greenbelt, MD, Feb. 26-28, 2002.
[paper ( PDF,196K)]

Bernd Fischer, Thomas Pressburger, Grigore Rosu, Johann Schumann, "The AutoBayes Program Synthesis System - System Description," Proc. CALCULEMUS 2001: 9th Symp. on the Integration of Symbolic Computation and Mechanized Reasoning, Siena, Italy, pp. 182-187, Jun. 21-22, 2001.
[papers ( PDF, 152K), ( Postscript, 284K)]

Bernd Fischer, Johann Schumann, "AutoBayes: A System for the Synthesis of Data Analysis Programs," Proc. NIPS 2000: Workshop on Software Support for Bayesian Analysis Systems, Breckenridge, CO, Dec. 1, 2000.
[papers ( PDF, 133K), ( Postscript, 275K)]

Wray Buntine, Bernd Fischer, Thomas Pressburger, "Towards Automated Synthesis of Data Mining Programs," Proc. KDD'99: 5th ACM Int'l Conf. on Knowledge Discovery and Data Mining, San Diego, CA, pp. 372-376, Aug. 15-18, 1999.
[papers ( PDF, 220K),( Postscript, 459K)]

Back to Top

AutoFilter: Synthesis of State Estimation Software

Jon Whittle, Johann Schumann, "Automating the Implementation of Kalman Filter Algorithms," TOMS: ACM Transactions on Mathematical Software, vol. 29, issue 5, pp. 434-453, Dec. 2004,
[papers ( PDF, 305K), ( Postscript, 273K)]

Grigore Rosu, Jonathan Whittle, "Towards Certifying Domain-Specific Properties of Synthesized Code," Proc. VCL'02: Third Int'l Workshop on Verification and Computational Logic, Pittsburgh, PA, pp. 46-56, Oct. 5, 2002.
[papers ( PDF, 104K), ( Postscript, 149K)]

Grigore Rosu, Jon Whittle, "Towards Certifying Domain-Specific Properties of Synthesized Code- Extended Abstract," Proc. ASE'02: 17th IEEE Int'l Conf. on Automated Software Engineering, Edinburgh, UK, pp. 289-294, Sep. 23-27, 2002.
[papers ( PDF, 79K),( Postscript, 108K)]

Jon Whittle, Jeffrey Van Baalen, Johann Schumann, Peter Robinson, Tom Pressburger, John Penix, Phil Oh, Michael Lowry, Guillaume Brat, "Amphion/NAV: Deductive Synthesis of State Estimation Software," Proc. ASE'01: 16th IEEE Int'l Conf. on Automated Software Engineering, San Diego, CA, pp. 395-399, Nov. 26-29, 2001.
[papers ( PDF, 129K), ( Postscript, 2.85M)]
UNPUBLISHED LONG VERSION [paper ( PDF, 2.82M)]

Johann Schumann, Peter Robinson, "[] or Success is Not Enough: Current Technology and Future Directions in Proof Presentation," Workshop IJCAR 2001: Int'l Joint Conf. on Automated Reasoning, Springer LNAI, no. 2083, Siena, Italy, pp. 702-710, Jun. 18-23, 2001.
[papers ( PDF, 1.6M), ( Postscript, 3.1M)]

Back to Top

UML Synthesis

Jon Whittle, Richard Kwan, Jyoti Saboo, "From Scenarios to Code: An Air Traffic Control Case Study," Proc. ICSE 2003: 25th Int'l Conf. on Software Engineering, Portland, OR, pp. 490-495, May 3-10, 2003.
[papers ( PDF, 209K),( Postscript, 499K)]

Jon Whittle, "Transformations and Software Modeling Languages: Automating Transformations in UML," Proc. UML 2002: Fifth Int'l Conf. on the Unified Modeling Language, Springer LNCS, no. 2460, Dresden, Germany, pp. 227-242, Sep. 30 to Oct. 4, 2002.
[papers ( PDF, 254K), ( Postscript, 398K)]

Jon Whittle, Johann Schumann, "Scenario-Based Engineering of Multi-Agent Systems," Chr. Rouff, ed., Formal Approaches to Agent Design, Springer, to appear.
[paper ( PDF, 1.5M)]

Johann Schumann, Jon Whittle, "Automatic Synthesis of Agent Designs in UML," Proc. FAABS 2001: First Int'l Workshop on Formal Approaches to Agent-Based Systems, Springer LNCS, no. 1871, Greenbelt, MD, pp. 148-162, Nov. 1, 2001.
[papers ( PDF, 249K), ( Postscript, 472K)]

Johann Schumann, Jon Whittle, "Automatic Synthesis of UML Designs from Requirements in an Iterative Process -Extended Abstract-," Proc. PMD'01: Workshop for Precise Modeling and Deduction for Object-Oriented Software Development, Siena, Italy, pp. 1-4, Jun. 18, 2001.
[paper ( PDF, 1.2M)]

Jon Whittle, Johann Schumann, "Generating Statechart Designs From Scenarios," Proc. ICSE 2000: 22nd Int'l Conf. on Software Engineering, Limerick, Ireland, pp. 314-323, Jun. 4-11, 2000.
[paper ( PDF, 217K)]

Back to Top

Certifiable Synthesis

Nurlida Basir, Ewen Denney, Bernd Fischer, "Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information". Proc. SAFECOMP '08: The 27th International Conference on Computer Safety, Reliability and Security. Newcastle, England, Sept. 22-25 2008.
[paper (PDF, 159K)]

Ewen Denney, Bernd Fischer,"Explaining Verification Conditions". Proc. AMAST '08: 12th International Conference on Algebraic Methodology and Software Technology. Urbana, Illinois, Jul. 28-31 2008.
[paper (PDF, 151K)]

Nurlida Basir, Ewen Denney, Bernd Fischer, "Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code," Proc. SafeCert '08: International Workshop on the Certification of Safety-Critical Software Controlled Systems, Budapest, Hungary, Mar. 29, 2008.
[paper (PDF, 101K)]

Ewen Denney, Steven Trac,"A Software Safety Certification Tool for Automatically Generated Guidance, Navigation and Control Code," Proc. IEEE Aerospace Conf., Big Sky, MT, Mar. 1-8, 2008.
[paper (PDF, 404K)]

Ewen Denney, Bernd Fischer,"Extending Source Code Generators for Evidence-based Software Certification," Proc. ISOLA '06: 2nd Int'l Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Paphos, Cyprus, Nov. 15-19, 2006.
[paper (PDF, 408K)]

Ewen Denney, Bernd Fischer,"A generic annotation inference algorithm for the safety certification of automatically generated code," Proc. GPCE'06: 5th Int'l Conf. 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," Proc. ASE'06: 21st IEEE/ACM Int'l Conf. on Automated Software Engineering, Tokyo, Japan, Sep. 18-22, 2006.
[paper (PDF, 63K)]

Ewen Denney, Bernd Fischer, Johann Schumann, "An Empirical Evaluation of Automated Theorem Provers in Software Certification," In Int'l Journal of AI Tools,Vol. 15, no. 1, pp. 81-107, Feb. 2006.
[paper ( PDF, 517K)]

Ewen Denney, Bernd Fischer, Dieter Hutter, Mark Jones, "2005 ASE Workshop on Software Certificate Management," Proc. SoftCeMent' 05: 2005 ASE Workshop on Software Certificate Management, Long Beach, CA, Nov. 8, 2005.
[paper (PDF, 1.8M)]

Ewen Denney, Bernd Fischer,"Software Certification and Software Certificate Management Systems," Proc. SoftCeMent'05: 2005 ASE Workshop on Software Certificate Management, Long Beach, CA, pp. 1-5, Nov. 8 2005.
[paper (PDF, 35K)]

Ewen Denney, Bernd Fischer, "Certifiable Program Generation," Proc. GPCE'05: 4th Int'l Conf. on Generative Programming and Component Engineering,Tallinn, Estonia, pp. 17-28, Sep.29 - Oct. 1, 2005.
[paper ( PDF, 103K)]

Ewen Denney, Bernd Fischer, "Formal Safety Certification of Aerospace Software," Proc. AIAA'05: Infotech at Aerospace, Arlington, VA, CD-ROM, Sep. 26 - 28, 2005.
[paper ( PDF, 427K)]

Geoff Sutcliffe, Ewen Denney, Bernd Fischer, "Practical Proof Checking for Program Certification," Proc. ESCAR'05: Empirically Successful Classical Automated Reasoning, Tallin, Estonia, Jul. 22-26, 2005.
[paper (PDF, 95K)]

Ewen Denney, Bernd Fischer, "A Program Certification Assistant Based on Fully Automated Theorem Provers," Proc. UITP'05: International Workshop on User Interfaces for Theorem Provers, Edinburgh, Scotland, pp. 98-166, Apr. 9, 2005.
[paper ( PDF, 1.3M)]

Julian Richardson, Johann Schumann, Bernd Fischer, Ewen Denney, " Rapid Exploration of the Design Space During Automatic Generation of Kalman Filter Code," Proc. IEEE Aerospace Conference, Big Sky, MT, CD-ROM, Mar. 5-12 2005.

Ewen Denney, Bernd Fischer, Johann Schumann, and Julian Richardson, "Automatic certification of Kalman filters for reliable code generation," Proc. IEEE Aerospace Conference, Big Sky, MT, CD-ROM, Mar. 5-12 2005.
[paper (PDF, 369K)]

Ewen Denney, Ram Prasad Venkatesan, "A Generic Software Safety Document Generator," Proc. AMAST 2004: 10th Int'l Conf. on the Algebraic Methodology and Software Technology, Springer LNCS, no. 3116, Stirling, Scotland, pp. 102-116, Jul. 12-16, 2004.
[papers ( PDF, 176K), ( Postscript, 213K)]

Ewen Denney, Bernd Fischer, Johann Schumann, "Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software," Proc. IJCAR 2004: Second Int'l Joint Conf. on Automated Reasoning, Cork, Ireland, pp. 198-212, Jul. 4-8, 2004.
[papers ( PDF, 162K), ( Postscript, 204K)]

Ewen Denney, Bernd Fischer, Johann Schumann, "Adding Assurance to Automatically Generated Code," Proc. HASE 2004: 8th IEEE Int'l Symp. on High Assurance Systems Engineering, Tampa, FL, pp. 297-299, Mar. 25-26, 2004.
[papers ( PDF, 51K), ( Postscript, 55K)]

Julian Richardson, Jeff Green, "Traceability Through Automatic Program Synthesis," Proc. TEFSE '03: 2nd Int'l Workshop on Traceability in Emerging Forms of Software Engineering, Montreal, Canada, Oct. 7, 2003.
[papers ( PDF, 38K), ( Postscript, 169K)]

Ewen Denney, Bernd Fischer, "Correctness of Source-Level Safety Policies," Proc. FME 2003: 12th Int'l Symposium of Formal Methods Europe, Pisa, Italy, pp. 894-913, Sep. 8-14, 2003.
[papers ( PDF, 234K),( Postscript, 285K)]

Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean, "Certifying Optimality of State Estimation Programs," Proc. CAV 2003: Conf. on Computer Aided Verification, Boulder, CO, pp. 301-314, Jul. 8-12, 2003.
[papers ( PDF, 165K),( Postscript, 586K)]

Johann Schumann, Bernd Fischer, Mike Whalen, Jon Whittle, "Certification Support for Automatically Generated Programs," Proc. HICSS'36: Hawaiian Int'l Conf. on System Sciences, Big Island, HI, pp. 337-339, Jan. 6-9, 2003.
[papers ( PDF, 106K),( Postscript, 206K)]

Grigore Rosu, Jonathan Whittle, "Towards Certifying Domain-Specific Properties of Synthesized Code," Proc. VCL'02: Third Int'l Workshop on Verification and Computational Logic, Pittsburgh, PA, pp. 36-45, Oct. 5, 2002.
[papers ( PDF, 104K),( Postscript, 149K)]

Grigore Rosu, Jon Whittle, "Towards Certifying Domain-Specific Properties of Synthesized Code -Extended Abstract-," Proc: ASE'02: 17th IEEE Int'l Conf. on Automated Software Engineering, Edinburgh, UK, pp. 289-294, Sep. 23-27, 2002.
[papers ( PDF, 79K), ( Postscript, 108K)]

Michael Whalen, Johann Schumann, Bernd Fischer, "AutoBayes/CC- Combining Program Synthesis with Automatic Code Certification -System Description-," Proc. CADE-18: Conf. on Automated Deduction, Springer LNCS, vol. 2392, Copenhagen, Denmark, pp. 290-294, Jul. 27-30, 2002.
[paper ( PDF, 156K)]

Michael Whalen, Johann Schumann, Bernd Fischer, "Synthesizing Certified Code," Proc. FME'02: 11th Int'l Symp. on Formal Methods Europe, Springer LNCS, vol. 2391, Copenhagen, Denmark, pp. 431-450, Jul. 22-24, 2002.
[paper ( PDF, 325K)]

Johann Schumann, "Automatic Synthesis of Safety-Related Software -Short Paper-," ACM SIGSOFT Software Engineering Notes, vol. 29, issue 2, pp. 105-108, Mar. 2002.
[paper ( PDF, 1.4M)]

Back to Top

Amphion: Synthesis of Planetary Software and Animations, and Theory Compilation

For Educators

This paper describes an application of Amphion to support educational web sites.

    Jane Friedman, Santos Gerardo Lazzeri, Thomas Pressburger, "Applying NASA Technology to Education, a Case Study Using Amphion," Proc: SITE 99: Society for Information Technology and Teacher Education 10th Int'l Conf., vol. 1999, issue 1, San Antonio, TX, pp. 1918-1923, Feb. 28 to Mar. 4, 1999.
    [paper ( PDF, 138K)]

For planetary scientists:

This paper describes an extension of Amphion/NAIF that generates science-opportunity visualizations.

    Michael Lowry, Thomas Pressburger, Steven Roach, "Animating Observation Geometries with Amphion," NASA Science Information Systems Newsletter, issue 35, pp. 35-38, Mar. 1995.
    [paper ( PDF, 572K)

This is the basic Amphion/NAIF paper.

    Michael Lowry, Andrew Philpot, Thomas Pressburger, Ian Underwood, Richard Waldinger, Mark Stickel, "Amphion: Automatic Programming for the NAIF Toolkit," NASA Science Information Systems Newsletter, issue 31, pp. 22-25, Feb. 1994.
    [paper ( PDF, 724K)]

For computer scientists:

These papers describe deductive synthesis, the domain theory, the user interface, and the architecture of the system.

    Jeffrey Van Baalen, Peter Robinson, Michael Lowry, Thomas Pressburger, "Explaining Synthesized Software," Proc. ASE'98: 13th IEEE Conf. on Automated Software Engineering, Honolulu, HI, pp. 240-248, Oct. 13-16, 1998.
    [papers ( PDF, 268K), ( Postscript, 1.57M)]

    Thomas Pressburger, Michael Lowry, "Automating Software Reuse with Amphion," NASA Workshop on Software Reuse, Fairfax, VA, Sep. 24-27, 1996.
    [paper ( PDF, 132K)]

    Michael Lowry, Thomas Pressburger, Andrew Philpot, "Automated Formal Methods for Component-Based Software Development," Int'l Workshop on Formal Methods Applications, Seattle, WA, Apr. 20-22, 1995.

This paper describes an extension that generates interactive search programs.

    Thomas T. Pressburger, Michael R. Lowry, "Automatic Domain-Oriented Software Design using Formal Methods," Proc: ETCE'95: Software Systems in Engineering, Energy-Source Technology Conf. and Exhibition,, Houston, TX, pp. 33-42, Jan. 29 to Feb. 1, 1995.
    [ abstract][papers ( PDF, 51K), ( Postscript, 197K)]

    Michael Lowry, Andrew Philpot, Thomas Pressburger, Ian Underwood, "Amphion: Specification-Based Programming for Scientific Subroutine Libraries," Proc. 3rd Int'l Symp. on Artificial Intelligence, Robotics, and Automation for Space,Pasadena, CA, pp. 41-44, Oct. 18-20, 1994.

    Michael Lowry, Andrew Philpot, Thomas Pressburger, Ian Underwood, "Amphion: Automatic Programming for Scientific Subroutine Libraries," Proc. ISMIS'94: 8th Int'l Symp. on Methodologies for Intelligent Systems, Charlotte, NC, pp. 326-335, Oct. 16-19, 1994.
    [ abstract] [papers ( PDF, 37K), ( Postscript, 158K)]

    Michael Lowry, Andrew Philpot, Thomas Pressburger, Ian Underwood, "A Formal Approach to Domain-Oriented Software Design Environments," Proc. KBSE'94: 9th Knowledge-Based Software Engineering Conf., Monterey, CA, pp. 48-57, Sep. 20-23, 1994.
    [ abstract] [papers ( PDF, 43K), ( Postscript, 202K)]

    Mark Stickel, Richard Waldinger, Michael Lowry, Thomas Pressburger, Ian Underwood, "Deductive Composition of Astronomical Software from Subroutine Libraries," Proc. CADE 94: 12th Int. Conf. on Automated Deduction, Springer LNAI, vol. 814, pp. 341-355, Jun. 26 to Jul. 1, 1994.
    [ abstract] [papers ( PDF, 169K), ( Postscript, 448K)]

This paper describes Amphion's text-based interface and summarizes the main concepts behind the client-server version of Amphion.

    Santos Lazzeri, "A Comparison of different HCI styles in a KBSE system," Proc. PROLAMAT 98: Tenth Int'l IFIP WG 5.2/5.3 Conf. on Programming Languages for Manufacturing, Trento, Italy, Sep. 9-12, 1998.
    [papers ( PDF, 145K), ( Postscript, 796K)]

These papers describe automated compilation of domain theories.

    Jeffrey Van Baalen, Steven Roach, "Using Decision Procedures to Build Domain-Specific Deductive Synthesis Systems," Proc. LOPSTR'98: 8th Int'l Workshop on Logic Program Synthesis and Transformation, Springer LNCS, vol. 1559, Manchester, U.K., pp. 71-80, Jun. 15-19, 1998.
    [papers ( PDF, 119K),( PostScript, 1.2M)]

    Jeffrey Van Baalen, Steven Roach, "Using Decision Procedures to Accelerate Domain-Specific Deductive Synthesis Systems," Proc. LOPSTR'98: 8th Int'l Workshop on Logic Program Synthesis and Transformation, Springer LNCS, vol. 1559, Manchester, U.K., pp. 61-70, Jun. 15-19, 1998.
    [papers ( PDF, 163K), ( Postscript, 1.7M)]

    Steven Roach, Jeffrey Van Baalen, Michael Lowry, "Meta-Amphion: Scaling up High Assurance Deductive Program Synthesis," Proc. HISS '97: IEEE High Integrity Software Symposium, Albuquerque, NM, pp. 81-93, Oct. 15-16, 1997.
    [papers ( PDF, 63K), ( Postscript, 195K)]

    Steven Roach, "TOPS: Theory Operationalization for Program Synthesis," PhD Thesis, University of Wyoming, August 1997.

    Michael Lowry, Jeffrey Van Baalen, "Meta-Amphion: Synthesis of Efficient Domain-Specific Program Synthesis Systems," Proc. KBSE '95: 10th Knowledge-Based Software Engineering Conf., Boston, MA, pp. 2-10, Nov. 12-15, 1995. AWARDED "BEST PAPER" AT CONFERENCE.
    [ abstract] [paper ( PDF, 48K), ( Postscript, 181K)]

This paper describes component understanding and reuse in the context of the NAIF libraries and Amphion.

    Spencer Rugaber, Kurt Stirewalt, Linda Wills, "Understanding Interleaved Code," Reverse Engineering, Kluwer Academic Publishers, vol. 3, no. 1/2, pp. 47-76, Jun. 1996.

Back to Top

Miscellaneous

    Daniel E. Cooke, Matt Barry, Michael Lowry, Cordell Green, "NASA's Exploration Agenda and Capability Engineering," IEEE Computer, vol. 39, no. 1, pp. 63-73 , Jan. 2006.

    Julian Richardson, Jeff Green, "Automating Traceability for Generated Software Artifacts," Proc. ASE'04: 19th IEEE Int'l Conf. on Automated Software Engineering, Linz, Austria, pp. 24-33, Sep. 20-24, 2004.
    [paper (PDF, 94K)]

    Julian Richardson, "Proof Planning and Program Synthesis: A Survey," Proc. AAAI 2002: Spring Symp. Workshop on Logic-Based Program Synthesis: State-of-the-Art, Future Trends,Technical Report SS-02-05, Palo Alto, CA, pp. 7-12, Mar. 25-27, 2002.
    [papers ( PDF, 127K),( Postscript, 119K]

    Julian Richardson, Pierre Flener, "Program Schemas as Proof Methods," Uppsala University Department of Information Technology Technical Report,no. 2003-008, Feb. 2003.
    [papers ( PDF, 916K),( Postscript, 182K]

    Bernd Fischer, Jonathan Whittle, "Integrating Deductive Retrieval into Deductive Synthesis," Proc. ASE'99: 14th Conf. on Automated Software Engingeering,Cocoa Beach, FL. pp. 52-62, Oct. 12-15, 1999.
    [papers ( PDF, 116K),( Postscript, 192K)]

    John Penix. "Rebound: A Framework for Automated Component Adaptation." Proc. WISR'99: 9th Annual Workshop on Software Reuse,Austin, TX, pp. 140-148, Jan. 7-9, 1999.
    [paper ( PDF, 131K)]

Back to Top

Last modified: Mar. 24, 2008 by Allen Dutra.