Automated proof checking tools have been successfully employed for the verification of digital systems. These tools have the advantage of being completely general but suffer from the inherent limits to the efficient automation of expressive logics. If the expressiveness is constrained) it is possible to define certain useful fragments of logic for which efficient decision procedures can be found. The paradigm of model-checking yields an important class of decision procedures for establishing temporal properties of finite automata. Model-checking is remarkably effective for automatically verifying finite automata with relatively small state spaces) but is inadequate when the state spaces are either too large or unbounded. For this reason) it is useful to integrate the complementary technologies of model-checking and proof checking. Such an integration has to be carried out in a delicate manner in order to be more than just the sum of the techniques. We describe an approach for such an integration where a BDD-based model-checker for the propositional mu-calculus has been used as a decision procedure within the framework of the PVS proof checker. We argue that our approach fits in nicely with the design philosophy of PVS of providing highly effective mechanical reasoning capability by using efficient decision procedures as the workhorses of an interactive proof checker.

• musimp.dvi
• musimp.ps