ACM Workshop on Strategic Directions in Computing Research
              Position Statement, Formal Methods Subgroup

                             John Rushby
                          SRI International

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.