Home : About Kestrel
 

Kestrel Institute is a non-profit computer science research institute focusing on formal and knowledge-based methods for incremental automation of the software 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 semantic component-based software; high-level specification languages; the analysis, synthesis, transformation, verification and visualization of both sequential and concurrent software. Such 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. Government agencies that fund Kestrel Institute's research include the Advanced Research Projects Agency, Rome Laboratory, the Air Force Office of Scientific Research, the Office of Naval Research, and the National Aeronautics and Space Administration.

Research Areas

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.

Software Engineering Environments

We are developing a formal environment model that allows the description of all objects, operations, and tools involved in software engineering environments. Based on such a model, we represent environment objects and their properties in a knowledge base. It will be possible within this framework to use our program transformation and synthesis technology to generate procedures to build new versions of a system, to generate releases, or to perform a maintenance step. Thus, by representing the life-cycle itself as a formal program, we can transform the life-cycle to achieve major optimizations.

Inference

Our design and synthesis systems require various forms of inference, such as finding necessary or sufficient conditions, simpler equivalents, or lower bounds. We are continuing to develop a deduction system that we have built to do this. 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 (e.g. C++, LISP).

Graphics

Graphical display of data is a large part of software systems and thus accounts for a significant portion of the cost of developing and maintaining software. We are working on a theoretical and practical basis for the generation of software for tabular and graphical displays. The effort consists of two theories to account for the generation of possible displays of given data, and the selection of an appropriate display for the task at hand.

Requirements

We attempt to 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

Here we attempt 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.

Analysis and Testing

Using automated inference techniques we attempt to analyze existing source code directly. Such analysis effects a partial symbolic execution of the code, from which we can extract semantic information useful in automated testing and re-engineering. Examples where inference allows us to use conservative assumptions to achieve immodest improvements upon current techniques include program slicing, test-case generation and infeasible path elimination.

- Back to Top -

- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -