Motivating Examples of Tool Interoperability

We outline some verification scenarios involving multiple tools and libraries.

There are certain verification tasks for which highly automated systems are the only practical solution. Typical automated systems include SAT solvers, temporal logic model checkers, and linear programming systems. For some other tasks, such tools are not applicable. This may be because of capacity constraints: even if the problem is solvable in principle, it's too big in practice. (For example, model-checking large functional blocks of a microprocessor.) More fundamentally, the verification task may go beyond what can in principle be solved using these techniques, e.g. because the state space is infinite or the specification involves exact real numbers.

In cases where the problem is not entirely solvable by automated systems, it is still desirable to delegate as much of it as possible to them. The most productive approach seems to be to use some high-level tools, under explicit user guidance to achieve some decomposition to subtasks that can be solved automatically. Typical examples are:

• Performing induction over time.
• Showing that a transition system is simulated by a finite-state one.
• Refining a clean mathematical specification with an executable one.

The need for a framework that supports such combinations has long been recognized. For example, a combination of general higher-order theorem proving with model checking and symbolic simulation forms the basis of the verification methodology applied to hardware verification at Intel.

*** Need to add many references and list explicit examples.