We are studying formal methods for specifying, deriving, and reasoning about concurrent systems. First, we are developing methods for specifying and proving the equivalence of program modules in open distributed systems. Specifically, we are studying high-level linguistic abstractions to express different kinds of specifications. Second, we are investigating methods for transforming such specifications into executable concurrent code. The methods will allow manipulation of both specification components and their derived program modules. The methods will therefore provide a formal basis for modular development of open distributed software systems.

Our object-oriented system architecture embodies the notion of customization to support particular hardware configurations and applications. Customization is structured through the use of inheritance. We have applied this approach to message passing systems, virtual memory, file systems, distributed virtual memory, scheduling, and machine-dependent software. Choices has, as its kernel, a dynamic collection of objects. It supports an object-oriented application interface based on local and distributed objects, inheritance, and polymorphism. The system is in use to evaluate specialized coscheduling, multicast messaging, distributed shared memory, and distributed file systems for parallel and continuous media distributed applications.

We are investigating a hybrid computer-assisted approach for confirming that the implementation of a system maintains its expected design models and rules. Our approach methodologically integrates logic-based static analysis and dynamic visualization. We show that the hybrid technique helps determine design-implementation congruence at many levels of abstraction, including concrete rules like coding guidelines, architectural models like design patterns or connectors, and subjective design principles like low coupling and high cohesion. The utility of our approach has been demonstrated in the development of microChoices, a new multimedia operating system which inherits many design decisions and guidelines learned from experience in the construction and maintenance of its predecessor, Choices.

Our goal in this work is to make accurate calendrical algorithms readily available, since calendrical problems are notorious for plaguing software. Information that is sufficiently detailed to allow computer implementation is difficult to find for many nonstandard calendars, since the published material is often inaccessible, ecclesiastically oriented, incomplete, inaccurate, based on extensive tables, overburdened with extraneous material, focused on shortcuts for hand calculation to avoid complicated arithmetic or to check results, or difficult to find in English. Most existing computer programs are proprietary, incomplete, or inaccurate.

This project involves the creation of an intelligent software design environment for construction of reliable programs. The environment will include a tool for development of formal specifications from constructive dialogues, tables, formulas, and other informal means. The specification aid will be capable of detecting missing or inconsistent information. A second aspect is the construction of tools to transform and augment specifications as a result of design decisions, and to provide assistance for implementation and code generation. These tools will check refinements for completeness and inconsistencies and provide machine assistance for avoiding common errors, generating routine code, enforcing coding standards, and formatting.

In large-scale software development, design occurs in an evolutionary manner. This is particularly true in object-oriented software development. During the design process many objects, relations, and other aspects of the system will change. Each change would necessitate other changes and may make the system inconsistent. It is usually the designers' responsibility to manage this change process. Managing this process, however, is a tedious and often complicated task. We are developing an automated support tool to assist with object change management. We address issues such as types of design change, semantics of change, formalization of change operators, and knowledge required for automated change management.

This project intends to study the form and use of a new abstraction method using data structure independent algorithm skeletons called task-oriented abstract algorithms (TOAA). These algorithm skeletons represent the essence of a common task, without the details that apply to special cases. Deciding what data structure to use in an abstract algorithm is part of its specialization and implementation information. Reusable software artifacts are most useful when they carry verification information. In our proposed method we anticipate partially verified reusable skeletons and correctness preserving specializations that provide the final proof of an implementation. The verification information includes assertions, data invariants, and restrictions on subtasks or data structure operations.

The major challenge in bringing functional languages into practice is compiling them into code that matches the efficiency of conventional languages. One approach to doing this is to mix functional and imperative features in a single language. However, such a language is much harder to compile than either a conventional or a functional language. We are studying static analysis methods for the compilation of one such language, the Imperative Lambda Calculus.

The goal of this project is the design, implementation (both sequential and parallel), and realistic application of a functional programming language supporting the development of scientific codes. Functional languages are characterized by two features higher-order functions and lazy evaluation which make them uniquely expressive and elegant, though at times inefficient. Scientific programming, on the other hand, demands great efficiency and has traditionally been done in FORTRAN. Design and implementation issues of these languages will be studied, and an application framework will be developed for the construction of programs in the domain of computerized tomography.

Many parts of the compiler-building process have been automated; lexing and parsing are the best-known examples. Significant success has also been achieved in automating the construction of code generators the part of a compiler that is directly concerned with the structure of a specific computer. This success has been achieved primarily for simple processors. This success has been achieved primarily for simple processors. We are exploring ways to represent the information needed to produce code generators for such processors in a tabular form. This will make code generators more portable and ease compiler development for new processors.

The Computing Research Laboratory continues to offer modern approaches to providing a flexible and convenient environment for computer science research. The current system is a hierarchical network of heterogeneous research networks, each suited to the needs of specific research groups. While the primary net provides common services to all researchers, each group network consists of specialized research computers and workstations. Newest additions to the research environment are ATM networking and multimedia computing. In the future, more specialized processors will be brought in to support the diverse research needs of the department and the fiber and ATM network will be extended.

This project investigates methodologies and automated tools for formal program derivation. The FOCUS system, the test bed for these methodologies, supports the paradigm of automation-based software development and maintenance. The software designer initially specifies the behavior of a system in a formal specification language. The specification language used in the FOCUS system is a higher-order functional logic language with recursive term data structures, sets, mappings, and relations. Such a specification can be executed using the FOCUS system and validated against customer requirements. The designer then systematically transforms the specification into an efficient program using the program derivation tools provided by the FOCUS system.