NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Towards High-Assurance High-Performance Program SynthesisDomain-specific automatic program synthesis tools, also called application generators, are playing an ever-increasing role in software development. However, high-performance application generators require difficult manual construction, and are very difficult to verify correct. This paper describes research and an implemented system that transforms program synthesis tools based on deductive synthesis into high-performance application generators. Deductive synthesis uses theorem-proving to construct solutions when given problem specifications. The verification condition for a deductive synthesis tool is essentially the soundness of the implemented inference rules. Theory Operationalization for Program Synthesis (TOPS) synergistically combines reformulation, automated mathematical classification, and compilation through partial deduction to decision procedures. It transforms general-purpose deductive synthesis, with exponential performance, into efficient special-purpose deductive synthesis, with near-linear performance. This paper describes our experience with and empirical results of PD(TH) theory-based partial deduction - in which partial deduction of a set of first-order formulae is performed within the context of a background theory. The implemented TOPS system currently performs a special variant of PD(TH) in which the compilation process results in the transformation of a set of first order formulae into the theory of an instantiated library decision procedure augmented by a compiled unit theory.
Document ID
19970029206
Acquisition Source
Ames Research Center
Document Type
Conference Paper
Authors
Lowry, Michael
(NASA Ames Research Center Moffett Field, CA United States)
Roach, Steven
(NASA Ames Research Center Moffett Field, CA United States)
vanBaalen, Jeffrey
(NASA Ames Research Center Moffett Field, CA United States)
Date Acquired
August 17, 2013
Publication Date
September 1, 1997
Publication Information
Publication: Fourth NASA Langley Formal Methods Workshop
Subject Category
Computer Programming And Software
Accession Number
97N27884
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
Document Inquiry

Available Downloads

There are no available downloads for this record.
No Preview Available