On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> INTRODUCTION <s> Although automated proof checking tools for general-purpose logics have been successfully employed in the verification of digital systems, there are inherent limits to the efficient automation of expressive logics. If the expressiveness is constrained, there are useful logic fragments for which efficient decision procedures can be found. The model checking paradigm yields an important class of decision procedures for establishing temporal properties of finite-state systems. 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. <s> BIB001 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> INTRODUCTION <s> We describe the verification of the IM: a large, complex (12000 gates and 1100 latches) circuit that detects and marks the boundaries between Intel architecture (IA-32) instructions. We verified a gate-level model of the IM against an implementation-independent specification of IA-32 instruction lengths. We used theorem proving to to derive 56 model-checking runs and to verify that the model-checking runs imply that the IM meets the specification for all possible sequences of IA-32 instructions. Our verification discovered eight previously unknown bugs. <s> BIB002 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> INTRODUCTION <s> Introduction.- Boolean Functions.- Finite State Machine Based Approaches.- Propositional Temporal Logics.- Higher Order Logic.- Appendix.- References.- Index.A more detailed table of contents can be found on our web site: http://www.springer.de <s> BIB003
State exploration method BIB003 (mainly model checking and equivalence checking) and Deductive verification (theorem proving) are two complementary approaches to formal verification of digital systems. In state exploration method, the design being verified is represented as a decision diagram and techniques such as reachability analysis are used to automatically verify that the properties of the design are satisfied against the model represented as a finite-state system. Thus, the verification of properties for finite-state systems is decidable. Much of this work is based on Binary Decision Diagrams  . Model checking is fully automatic and can also provide counter-examples when the verification of properties fails but suffers from the so-called state space explosion problem when dealing with complex systems. In deductive theorem proving method, the correctness of a design is explored as a theorem in a mathematical logic and the proof of the theorem is checked using a general-purpose theorem-prover. Deductive theorem proving is a scalable technique that can handle complex designs and reason formally about unbounded data structures that make systems infinitestate. It provides relatively complete proof systems but requires skilled manual guidance for verification and human insight for debugging. Unfortunately, if the property fails to hold, deductive methods do not give counter-example. There has been a great deal of work over the past decade to combine the two approaches to gain the strengths of both, and alleviate the weaknesses. A common approach is to use a state exploration method as an oracle which makes the proof and returns answer to the theorem prover. Successful combinations of this kind have been achieved in BIB002     BIB001  . The strengths and weaknesses of model checking and deductive theorem proving, as discussed above, are summarized in (Table.1 ). Diagrams algorithms to theorem provers. A comparison between both is discussed in detail. The paper also tries to answer which is the best decision graphs formalization for theorem provers as what is the optimized set of operations to efficiently manipulate the decision graphs inside theorem provers. Then, we contrast between them according to their efficiency, complexity and feasibility.