Formal methods have gained acceptance in the hardware field through a pragmatic approach that has succeeded in providing systematic, scalable, highly automated, and cost effective treatments for certain stereotypical problems of practical importance. By identifying stereotypical problems, the effort required to develop effective formal methods has been amortized over many applications. We suggest that formal methods can achieve similar industrial success in selected software applications by following the same principles. As an illustration, we examine approaches to the stereotypical problem of interpreter correctness in the presence of timing differences between the specification and implementation interpreters. In hardware, this corresponds to the problem of verifying microprogrammed, pipelined, or superscalar processors, but it has wider applications to any system-hardware or software-that can be considered as an interpreter.

The effectiveness of hardware verification techniques has increased markedly in the past decade. As hardware verification techniques become increasingly powerful the idea of transitioning verification technology to industry can be taken seriously. Nevertheless, powerful decision procedures that can completely automate the verification of certain types of hardware, whether they are BDD based model-checkers or automatic microprocessor verification tools, cannot be adequate on their own for industrial hardware verification. However, a high-level, general-purpose theorem prover with specific capabilities can provide an overall framework in which these tools can be embedded and in which they can then be effectively used for industrial hardware verification.