On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.2: Embedding Model Checking inside Theorem Proving Tool <s> Binary Decision Diagrams (BDDs) are a representation for Boolean formulas which makes many operations, in particular tautology - checking, surprisingly efficient in important practical cases. In contrast to such custom decision procedures, the HOL theorem prover expands all proofs out to a sequence of extremely simple primitive inferences. In this paper we describe how the BDD algorithm may be adapted to comply with such strictures, helping us to understand the strengths and limitations of the HOL approach. <s> BIB001 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.2: Embedding Model Checking inside Theorem Proving Tool <s> Two methods of programming BDD-based symbolic algorithms in the Hol98 proof assistant are presented. The goal is to provide a platform for implementing intimate combinations of deduction and algorithmic verification, like model checking. The first programming method uses a small kernel of ML functions to convert between BDDs, terms and theorems. It is easy to use and is suitable for rapid prototying experiments. The second method requires lower-level programming but can support more efficient calculations. It is based on an LCF-like use of an abstract type to encapsulate rules for manipulating judgements ρ t → b meaning "logical term t is represented by BDD b with respect to variable order ρ". The two methods are illustrated by showing how to perform the standard fixed-point calculation of the BDD of the set of reachable states of a finite state machine. <s> BIB002 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.2: Embedding Model Checking inside Theorem Proving Tool <s> Model Checking is an algorithmic technique to determine whether a temporal property holds of a program. For linear time properties, a model checker produces a counterexample computation if the check fails. This computation acts as a "certificate" of failure, as it can be checked easily and independently of the model checker by simulating it on the program. On the other hand, no such certificate is produced if the check succeeds. In this paper, we show how this asymmetry can be eliminated with a certifying model checker. The key idea is that, with some extra bookkeeping, a model checker can produce a deductive proof on either success or failure. This proof acts as a certificate of the result, as it can be checked mechanically by simple, non-fixpoint methods that are independent of the model checker. We develop a deductive proof system for verifying branching time properties expressed in the mu-calculus, and show how to generate a proof in this system from a model checking run. Proofs for linear time properties form a special case. A model checker that generates proofs can be used for many interesting applications, such as better ways of exploring errors in a program, and a tight integration of model checking with automated theorem proving. <s> BIB003 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Fig.2: Embedding Model Checking inside Theorem Proving Tool <s> Model checking and theorem proving are two complementary approaches to formal verification. In this paper we show how binary decision diagram (BDD) based symbolic model checking algorithms may be embedded in a theorem prover to take advantage of the comparatively secure environment without incurring an unacceptable performance penalty. <s> BIB004
The result of the model checker is correct by construction, since both of the theory and the implementation are proved correct in the theorem prover. Thus soundness is guaranteed because more work is backed up by mechanized fully-expansive proof. The price for the extra proof and flexibility is in increased development effort. The "deep embedding" approach  introduce the decision graph syntax as a new higher order logic type and then define the operations and algorithms based on this syntax within the theorem prover. This contrasts within a "shallow embedding" where the syntax is not formally represented in the logic, only in the metalanguage. In general, a deep embedding allows one to reason about the language itself rather than just the semantics of programs in the language. Gordon BIB002 integrated the BDDs based verification system BuDDY into HOL by implementing the primitive BDDs operations as inference rules added to the core of the theorem prover. The author used a small kernel of ML functions to convert between BDDs, terms and theorems. As long as those primitives are correct, it was possible to achieve the advantages of both theorem proving tools and decision diagram algorithms without the need to trust a complete external package, just a set of primitives. The aim of using BuDDy is to get near the performance of C-based model checking by using BDDs package implemented in C, whilst remaining fully expansive, though with a radically extended set of inference rules [34] . In BIB001 , Harrison implemented BDDs inside the HOL system without making use of external oracle. The BDDs algorithms were used by a tautologychecker; however, the author found that the performance was about thousand times slower than with BDDs engine implemented in C. The author argued that by re-implementing some of HOL's primitive rules, performance could be improved by around ten times. Amjad BIB004 demonstrated how BDDs based symbolic model checking algorithms for the propositional µ calculus µ L can be embedded in the HOL theorem prover. His approach allows results returned from the model checker to be treated as theorems in HOL. By representing primitive BDDs operations as inference rules added to the core of the theorem prover, the execution of a model checker for a given property is modeled as a formal derivation tree rooted at the required property. These inference rules are hooked to a high performance BDDs engine [34] external to the theorem prover. The approach still leaves results reliant on the soundness of the underlying BDDs tools. Thus, the security of the theorem prover is compromised only to the extent that the BDDs engine or the BDDs inference rules may be unsound. In  , the authors followed a similar approach to the BuDDy work [34] but embedding MDGs rather than BDDs and inside HOL rather than using ML. They provided a complete formalization of the MDGs logic and its well-formedness conditions as DFs in HOL mechanically. Based on this infrastructure they formalized the basic MDGs operations in HOL following a deep embedding approach and proved their correctness. Their aim is to embed the MDGs model checker in the HOL theorem prover. Whereas BIB004 approach relies on the BDDs computations carried out by BDDs primitive inference rules,  work focuses more on how one can raise the level of assurance by embedding and proving formally the correctness of those operators in HOL. In BIB003 , the author showed a mechanism of how certifying model checker can be constructed. The idea is that, a model checker can produce a deductive proof on either success or failure. The proof acts as a certificate of the result, since it can be checked independently. A certifying model checker thus provides a bridge from the model-theoretic to the prooftheoretic approach to verification. The author developed a deductive proof system for verifying branching time properties expressed in the µ -calculus, and showed it to be sound. Then, a proof generation in this system from a model checking run is presented. In  , the authors successfully carried out the verification of the model checker RAVEN. RAVEN is a real-time model checker which uses time-extended finite state machines (interval structure) to describe systems and a timed version of CTL (CCTL) to describe properties. Optimized algorithms based on an extended characteristic functions are used to compute the extension sets. The specification and the correctness proof were carried out using an interactive specification and verification system KIV.