This award supports research in deductive methods, applied to automate the synthesis of software built from component libraries. Software is constructed from relatively large-scale components, rather than from the primitive instructions of a programming language. Theorem-proving techniques are invoked to identify the relevant components and to compose them to solve the problem at hand. The goal is to put computing power in the hands of a broader segment of the population and to increase the productivity and accuracy of the expert practitioner. The software is constructed to meet specifications expressed in a logical or graphical notation. Specifications are elicited from the user via a dialog with a graphical user interface. The specification is phrased as a mathematical theorem, which is proved by an automatic deduction system. The proof is conducted in an application domain theory, which describes the components in the software library, the constructs of the specification language, and the background knowledge necessary to glue the components together to meet the specification. The theorem is proved by the automatic deduction system Snark, which has been implemented for applications in software engineering and artificial intelligence. A program that meets the original specification is extracted from the proof and translated into the desired target language. Software is produced with high assurance of correctness---it is verified by the proof from which it is extracted. This research is expected to make subroutine libraries, component libraries, and software reuse libraries accessible to users who are largely ignorant of the contents of the libraries, their conventions and terminology, or even the target programming language.
