Kestrel Institute is a non-profit computer science research center focusing on formal and knowledge-based methods for the automation of the software development process. Kestrel's research efforts are applicable to the construction of the intelligent software design and engineering environment of the future that provides automated support for all activities in the software life-cycle. Toward this goal, we carry out research on high-level specification languages, domain-specific languages, refinement, transformations, synthesis, analysis, and verification. Knowledge-based systems for software development and maintenance will significantly improve software productivity, reliability, manageability, and efficiency. The use of these automated tools will mitigate much of the complexity that makes software creation and maintenance difficult and expensive.
Our staff of researchers combines expertise in program synthesis, software engineering, machine intelligence, knowledge-base management, logic, automated reasoning systems, software environments, programming languages, and compilers. Kestrel Institute's research is funded by the Department of Defense, the Defense Advanced Research Projects Agency, the Intelligence Advanced Research Projects Activity, the Air Force Rome Laboratories, the Air Force Office of Scientific Research, the Office of Naval Research, the National Aeronautics and Space Administration, the GE Global Research Center, the Ethereum Foundation, and the Decentralization Foundation.
- Algorithm Design
- A few fundamental algorithm schemes, such as generate-and-test, branch-and-bound, divide-and-conquer, dynamic programming, and hill-climbing, explain a great number of known algorithms. We are codifying these algorithm design schemes so that these kinds of algorithms can be automatically derived for a given very-high-level problem specification, when given appropriate domain axioms.
- Transformational Compilation
- Our work is concerned with techniques for optimizing algorithms. We have been investigating performance-estimation-guided data structure synthesis, finite differencing (a generalization of traditional strength reduction), loop fusion, iterator inversion, and constraint compilation.
- Our design and synthesis systems require various forms of inference, such as finding necessary or sufficient conditions, simpler equivalents, or lower bounds. We are developing deduction systems that carry out these forms of inference. We are also investigating algorithms for constraint satisfaction and special purpose reasoning.
- Language Design
- A central issue is the design of very-high-level and wide-spectrum languages, for specifying both programs and software knowledge in general. We are investigating languages for specifying and transforming software architectures and frameworks, algorithm classes and schemas, abstract data types, concurrency constructs, reactivity, and program optimizations. Key to our goals are languages which are scalable and support both high-level, easy-to-understand specifications, and the incremental refinement of such specifications into efficient, error-free, executable code in a variety of target languages.
- We apply the results of our research on language design, time models, and graphics to the specification of functional, performance, and interface requirements. Together with domain-specific synthesis (below), emerging tools will considerably speed up requirements convergence.
- Domain-Specific Synthesis
- Our goal is to codify knowledge that is specific to a particular application area so that the transformation system can use this knowledge during the refinement of specifications written in a domain-specific language. Much like a module encapsulates a particular data type or algorithm, we introduced the notion of a knowledge pack that encapsulates generic, reusable concepts needed to specify and to solve problems in a particular application domain.