Engineering topics

VanBaalen, Jeffrey

Publications and source records attributed to VanBaalen, Jeffrey.

5 records

NASA NTRS1999

Transformation Systems at NASA Ames

In this paper, we describe the experiences of the Automated Software Engineering Group at the NASA Ames Research Center in the development and application of three different transformation systems. The systems span the entire technology range, from deductive synthesis, to logic-based transformation, to almost compiler-like source-to-source transformation. These systems also span a range of NASA applications, including solving solar system geometry problems, generating data analysis software, and analyzing multi-threaded Java code.

Buntine, Wray↗

NASA NTRS1998

Using Decision Procedures to Build Domain-Specific Deductive Synthesis Systems

This paper describes a class of decision procedures that we have found useful for efficient, domain-specific deductive synthesis. These procedures are called closure-based ground literal satisfiability procedures. We argue that this is a large and interesting class of procedures and show how to interface these procedures to a theorem prover for efficient deductive synthesis. Finally, we describe some results we have observed from our implementation. Amphion/NAIF is a domain-specific, high-assurance software synthesis system. It takes an abstract specification of a problem in solar system mechanics, such as 'when will a signal sent from the Cassini spacecraft to Earth be blocked by the planet Saturn?', and automatically synthesizes a FORTRAN program to solve it.

VanBaalen, Jeffrey↗

NASA NTRS1998

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 proof structures and abstracts them to provide explanations of the relation between a specification, a domain theory, and synthesized code. In generating these explanations, the tool exploits the structure of Amphion domain theories, so the end user is not confronted with the intricacies of raw proof traces. This tool is crucial for the validation of domain theories as well as being important in everyday use of the code synthesis system. It plays an important role in validation because when generated programs exhibit incorrect behavior, it provides the links that can be traced to identify errors in specifications or domain theory. It plays an important role in the everyday use of the synthesis system by explaining to users what parts of a specification or of the domain theory contribute to what pieces of a generated program. Comments are inserted into the synthesized code that document these explanations.

VanBaalen, Jeffrey↗

NASA NTRS1997

Automated Reuse of Scientific Subroutine Libraries through Deductive Synthesis

Systematic software construction offers the potential of elevating software engineering from an art-form to an engineering discipline. The desired result is more predictable software development leading to better quality and more maintainable software. However, the overhead costs associated with the formalisms, mathematics, and methods of systematic software construction have largely precluded their adoption in real-world software development. In fact, many mainstream software development organizations, such as Microsoft, still maintain a predominantly oral culture for software development projects; which is far removed from a formalism-based culture for software development. An exception is the limited domain of safety-critical software, where the high-assuiance inherent in systematic software construction justifies the additional cost. We believe that systematic software construction will only be adopted by mainstream software development organization when the overhead costs have been greatly reduced. Two approaches to cost mitigation are reuse (amortizing costs over many applications) and automation. For the last four years, NASA Ames has funded the Amphion project, whose objective is to automate software reuse through techniques from systematic software construction. In particular, deductive program synthesis (i.e., program extraction from proofs) is used to derive a composition of software components (e.g., subroutines) that correctly implements a specification. The construction of reuse libraries of software components is the standard software engineering solution for improving software development productivity and quality.

Lowry, Michael R.↗

NASA NTRS1992

The Role of Reformulation in the Automatic Design of Satisfiability Procedures

Recently there has been increasing interest in the problem of knowledge compilation (Selman & Kautz91). This is the problem of identifying tractable techniques for determining the consequences of a knowledge base. We have developed and implemented a technique, called DRAT, that given a theory, i.e., a collection of firstorder clauses, can often produce a type of decision procedure for that theory that can be used in the place of a general-purpose first-order theorem prover for determining many of the consequences of that theory. Hence, DRAT does a type of knowledge compilation. Central to the DRAT technique is a type of reformulation in which a problem's clauses are restated in terms of different nonlogical symbols. The reformulation is isomorphic in the sense that it does not change the semantics of a problem.

VanBaalen, Jeffrey↗