Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction (RI) is a method for inductive theorem proving proposed by Reddy. In order to obtain successful proofs, it is very important to choose appropriate contexts (such as in which direction each equation should be oriented) when applying RI inference rules. If the choice is not appropriate, the procedure may diverge or the users have to come up with several lemmas to prove together with the main theorem. Therefore we have a good reason to consider parallel execution of several instances of the rewriting induction procedure, each in charge of a distinguished single context in search of a successful proof. In this paper, we propose a new procedure, called multi-context rewriting induction, which efficiently simulates parallel execution of rewriting induction procedures in a single process, based on the idea of the multi-completion procedure. By the experiments with a well-known problem set, we discuss the effectiveness of the proposed procedure when searching along various contexts for a successful inductive proof.

This paper describes the results obtained of a prototype system, VeriProc/1, based on an algorithm we first presented in [13] which can prove the correctness of pipelined processors automatically without pipeline invariant, human interaction, or additional information. No timing relations such as an abstract function or β-relation is required. The only information required is to specify the location of the selectors in the design. The performance is independent of not only data width but also memory size. Detailed analysis of CPU time is presented. Further, don't-care forcing using additional data easily prepared by the user can improve performance.