One of the most promising directions for development of verification systems is the integration of tools and techniques that have developed in diverse domains. We are beginning to see theorem provers that integrate inductive proof techniques, general rewrite procedures, model checking, propositional provers (such as the BDD method considered earlier), linear arithmetic, other decision procedures, tactic facilities, execution capabilities, enhanced static checking, lemma generation, and computer algebra systems. These are not yet all in one system, nor is it clear how to optimize joint use, but the benefits of success are clear. Some systems that are partially successful in combining techniques are PVS, Nqthm, ACL2, HOL, EVES [29] [30], and RRL. PVS is particularly aggressive about integrating many of these tools, with quite impressive results. The linking of systems is also occurring. The verification of the SCI cache coherency protocol mentioned earlier uses a linking of HOL and Nuprl, which allows many theorems from HOL to be imported into Nuprl. The linking is a nontrivial task that took several years of theoretical ground work [50] because of the different formulations of higher-order logic each system uses. The gain from all this theoretical effort is the ability to use the deductive aspects of each where each is strong.
Another important development direction is the continued automation of verification procedures, almost all of which have strong dependence on highly skilled user input. This automation task is very difficult in general, of course, and research has been steadily pushing on the boundaries of this problem. Progress is being made at the edges of the problem, such as type-checking and array-bound checking. (SIMPLIFY is a system that uses simple decision procedures to find bugs in MODULA-3 programs [38]. While bug-finding is not verification, it is another illustration that some program analysis tasks can be automated now by AD-related techniques.)
Big gains in automation of verification systems are likely from the combination of computer algebra and AD systems, although problems exist. The possible gains are illustrated by Analytica. Analytica runs in fully automated mode. Although it does not handle the complexity of proof arguments of a good interactive system, it surpasses almost all fully automated verifiers not using computer algebra. However, there are problems of soundness (correctness) in all the major commercial computer algebra systems--Mathematica, Maple, Macsyma--which is disturbing. AD research can help here, as we discuss later.
Increased automation of induction proofs would also realize big gains for verification systems. Progress is being made, but this is a long-range problem; we discuss it briefly under the paragraph on mathematics. Much of the progress to date has been made by researchers addressing the verification problem specifically. There are advantages to addressing the automatic generation of induction hypotheses (one of the most creative tasks in deductive mathematics) within the verification setting because verification tasks have certain forms that allows specialization of the induction hypothesis methods. Also, verification proofs are shallower (but messier) than general mathematical proofs. These characteristics are reasons why research specifically in verification must be pursued, and not resisted with the expectation that general AD research will provide the solution. Rather, the overall message of forty years of research in AD is that when an important special task can be identified, then research should focus on that special task.
AD technology may be able to enhance the capability of the model checking method. The application of induction techniques could allow the checking of parameterized systems by generalized model checking. Indeed, this has already been accomplished in one manner in the PVS system by viewing model checking as a decision procedure for a finite (fixed point) subcalculus of the PVS higher-order logic. An important application would be the use of a theorem prover to verify the abstraction mapping of a large system to a smaller finite-state machine. Then model checking could be used to check the abstract machine. As an extension of this idea, systems might be decomposed for processing by model checkers with the composition of the components verified by a theorem prover. It is likely that the theorem-proving part would be done interactively for some time into the future, whereas the checking of the abstraction could then be done fully automatically by model checking.