Explaining Synthesized Software

9 years 4 months ago
Explaining Synthesized Software
Motivated by NASA's need for high-assurance software, NASA Ames' Amphion project has developed a generic program generation system based on deductive synthesis. Amphion has a number of advantages, such as the ability to develop a new synthesis system simply by writing a declarative domain theory. However, as a practical matter, the validation of the domain theory for such a system is problematic because the link between generated programs and the domain theory is complex. As a result, when generated programs do not behave as expected, it is difficult to isolate the cause, whether it be an incorrect problem specification or an error in the domain theory. This paper describes a tool we are developing that provides formal traceability between specifications and generated code for deductive synthesis systems. It is based on extensive instrumentation of the refutation-based theorem prover used to synthesize programs. It takes augmented ructures and abstracts them to provide expla...
Jeffrey Van Baalen, Peter Robinson, Michael R. Low
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where KBSE
Authors Jeffrey Van Baalen, Peter Robinson, Michael R. Lowry, Thomas Pressburger
Comments (0)