Kestrel's work on automated software development stems from a variety of sources (in various fields).

Deductive Synthesis in Artificial Intelligence – the field of Automatic Programming was once prominent in AI.  Cordell Green's and Richard Waldinger's theses in 1968 laid out key ideas of deductive program synthesis – generating programs by extracting them from proofs that their specification is valid.  The theme of closely integrating program development and theorem-proving continues to the present. 

CLEAR – In the CLEAR proposal, Goguen and Burstall  provide a category theoretic foundation for software development.  Specifications are the objects of interest and their morphisms show how to preserve specification structure and properties.  Colimits are used to build larger specifications out of smaller ones and to instantiate parameterized specifications.  Specware is a descendant of CLEAR with an additional focus on refinement of specifications, automation, and integration with theorem provers. 

Program Transformation -- Kestrel’s work in the 1980’s centered  around tools for program transformation as a way to support application development, code migration, and compiler construction.  The CHI prototype led to the founding of Reasoning Systems and the commercial Refine system.   Ideas from Refine are finding their way into OMG standards for code modernization.  Refine was also used as a basis for developing Kestrel research prototypes including the KIDS and DTRE systems, as well as first versions of Specware.

Knowledge Representation in Artificial Intelligence – The representation of expert design knowledge has been a recurring theme at Kestrel.  Taxonomies of domain theories, algorithm theories, data type refinements, and program optimization transformations capture at a precise but abstract level the kinds of knowledge that experts bring to bear in designing programs.

References

R. M. Burstall and J. A. Goguen, Putting Theories Together to Make Specifications, Proceedings of the Fifth International Joint Conference on Artificial Intelligence, Cambridge, MA, pp 1045-1058, 1977.

R. M. Burstall and J. A. Goguen, The semantics of {CLEAR}, a specification language, Proceedings, 1979 Copenhagen Winter School on Abstract Software Specification, Ed. D. Bjorner,  Springer LNCS 86, 1980.

Cordell Green,  Application of Theorem Proving to Problem Solving, Proceedings of the First International Joint Conference on Artificial Intelligence, 1969, pp 219—239.

Richard Waldinger, Constructing Programs Automatically Using Theorem Proving, Dept. of Computer Science, Carnegie-Mellon University, Pittsburg, PA, 1969.