ACM Computing Surveys 28(4es), December 1996, http://www.acm.org/pubs/citations/journals/surveys/1996-28-4es/a123-rushby/. Copyright © 1996 by the Association for Computing Machinery, Inc. See the permissions statement below. This article derives from a position statement prepared for the Workshop on Strategic Directions in Computing Research.

John Rushby

Formal methods contribute useful mental frameworks, notations, and systematic methods to the design and documentation of computer systems, but the primary benefit from specifically formal methods is that they allow certain questions to be settled by symbolic calculation--that is, by formal deduction and related methods such as model checking. In short, it's the tools that make formal methods useful.

Formal methods have started to attract mainstream interest in some fields (notably hardware) because their use has become cost-effective: they can now deliver valuable results at an acceptable price. This is due to several factors: a more pragmatic approach (applying formal methods to only part of a design, and for debugging as much as for correctness), systematic application (so that treatments suitable for specific topics--such as cache coherence, or pipeline correctness--have become well developed), and technical advances (e.g., breakthroughs such as symbolic model checking and more modest, but sustained, progress in theorem proving).

There are weaknesses, however, in these generally promising developments. Many of the techniques and supporting tools are narrow in their range of application, so that moving to a new problem requires developing a new technique, tinkering with a tool, or doing a lot of ad-hoc and informal "reduction" from the natural problem statement to one that can be dispatched by an available technique. The notations used to support efficient methods of symbolic calculation are often less than ideal as specification languages for human communication. And it is seldom possible to combine different methods in any but the clumsiest ways.

I believe that an important research topic is the development of integrated methods and tools that will make it possible to bring the resources of several techniques to bear on a single problem. By this, I do not mean crude connections such as "combine language X with theorem prover Y" (or the variant that used to be heard some years ago: define common intermediate representation A so that I can use X with both Y and Z), but more intimate integrations that, for example, allow model checking to be used as an element in theorem proving. Technical topics in support of this agenda include development of efficient decision procedures for important special theories such as bitvectors and queues (and the recasting of effective specialized methods such as BMDs and (word-level) model checking as decision procedures) that can be slotted into an existing theorem prover in such a way that they cooperate harmoniously with its existing capabilities; mechanized support for the development of invariants and abstractions; and the harnessing of these resources to more types of analysis than just verification and refutation (e.g., direct execution, simulation, fault-tree analysis).

These topics require research as well as engineering, and will produce significant incremental advances; sustained for a decade, they could provide a breakthrough in the utility of mechanized formal methods.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.