John V. Guttag - US grants

There is now widespread agreement that precise specifications can play an important role in software development and maintenance. It is less clear that formal specification, as opposed to precise informal specifications, are worth the extra effort required to create them. Proponents of formal specifications have argued that their susceptibility to machine analysis and manipulation increases their value and reduces their cost. This project is trying to support this claim by building and using tools that aid in the construction of formal specifications for programs and program modules. The specification languages that have been used permit significant assertions about logical properties of specifications--properties related to consistency, completeness, and module independence--to be made. Experience in hand checking specifications has lead to the conviction that such assertions are useful in establishing the validity of a specification. Unfortunately, these assertions cannot be checked completely by machine because they are all undecidable in the general case. Hence, this project will: do the theoretical work necessary to design useful approximations to these checks; implement a specification system that incorporates these approximations, building upon an existing syntax-directed editor and term-rewriting laboratory; evaluate these tools by using them to write specifications; and report on this experience, paying particular attention to the merits of formal vs. precise informal, and definitional vs. operational, specifications.

This research is based on the Larch family of specification languages, which support a two-tiered definitional approach to specification. Each specification has components written in two languages: one designed for a specific programming language and another common to all programming languages. The former are called Larch interface languages, and the latter the Larch Shared Language. Prior work has concentrated on the Shared Language. The new work shifts attention to interface languages; providing precise semantics for these languages, using them to write substantial interface specifications, determining what checking should be applied to these specifications, and developing tools for performing these checks.

This award will support collaborative research in software engineering between Drs. John Guttag and Stephen Garland, Massachusetts Institute of Technology and Drs. Michel Bidoit and Christine Choppy, Laboratoire de Recherche Informatique, University of Paris-Sud, France. The investigators propose a joint project that will first work on combining Assegigue, a specification environment under development at the University of Paris-Sud, and LP, a theorem proving system under development at MIT. They will then experiment with using the combined system to develop and reason about specifications. There is now widespread agreement that precise specifications can play a useful role in software development and maintenance. The most vexing problems in building systems deal with overall system organizations and the integration of components. Modularity is the key to controlling this, and specifications are essential for achieving modularity. Both the US and French research groups have adopted a style of specification that emphasizes brevity and clarity rather than executability. To make it possible to test specifications without executing or implementing them, both groups have developed techniques that enable specifiers to make claims about logical properties of specifications. However, whereas the French have centered their research around the technology needed to produce and manage large scale specifications, the MIT group has centered its research around the technology needed to check claims about logical properties of specification. By combining these two complementary research efforts, the investigators plan to produce a tool that can be used to develop, reason about and manage large-scale formal specifications of software.

Today, tools are needed to support and promote the use of formalisms in designing software interfaces concurrent algorithms, and digital circuits. Such tools must provide assistance with assessing the semantic content of designs, not just with their syntax. This project involves development of one such tool, the Larch Prover (LP). Current applications of LP include debugging Larch specifications, reasoning about circuit designs, and reasoning about concurrent algorithms. The project will continue developing LP in support of these and other applications, e.g., reasoning about specification in Larch and other specification languages, making use of specifications in optimizing compilers, and verifying locking levels in Modula-3. The project will develop front ends to serve as interfaces between these applications and LP. It will also enhance LP to serve better as a back end for such applications. Projected enhancements to LP include more general quantification, additional inference mechanisms (congruence closure, decision procedures for linear orders), and further assistance for handling complex proofs ( scoping, polymorphism, proof management). These enhancements will be driven by the demands of applications: they will be made within a context that is oriented towards debugging proofs and that emphasizes ease of interaction, good performance, proof strategies based on simplification, and replayable proof scripts.

The Larch Workshop is intended to bring together international users and developers of the Larch family of specification languages and tools. The three-day workshop, organized by Professors Ursula Martin (European coordinator) and Jeannette WIng (US coordinator) will be the first meeting ever of those who have over the past 11 years designed the Larch languages, built tool support for them, and used them to specify and reason about software and hardware systems. The group includes users and developers of the Larch Prover (LP), one of the Larch tools that distinguishes Larch from its competitors in formal methods. The invited participants include researchers from the United States and Europe who are active in the area of formal specification and verification. The workshop will be held at Endicott House, approximately 15 miles from MIT, in Dedham, Massachusetts. The award is pursuant to the NSF-ESPRIT agreement.

The project assesses patient cardiovascular risk and matches patients to the treatments most likely to be effective. The project addresses this problem through sophisticated computational methods that identify new markers of disease, improve the ability to measure both new and existing markers, and construct personalized models that can provide highly accurate assessments of individual risk. The core focus of the research addresses the poor performance of existing tools for cardiovascular decision support through advanced methods at the intersection of machine learning, data mining, signal processing, and applied algorithms; with the research guided by knowledge of cardiac pathophysiology.

This project impacts patient care for a disease that causes roughly one death every 38 seconds in the United States and imposes a burden of over half a trillion dollars in the U. S. each year. More generally, many of the ideas explored here (e.g., personalization of risk models) extends to a wide variety of other disorders in a straightforward manner and leads to wide improvements in outcomes while controlling costs. The research also strengthens interdisciplinary research in EECs and medicine throughout the computer science research community.