On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> The programming of a proof procedure is discussed in connection with trial runs and possible improvements. <s> BIB001 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> This paper describes a simple graph theory expressed in higher order logic and the applications of it in railway signalling. A theory of network based on the graph theory is developed to model the stalic aspects of railway track networks. Tools are being developed to produce formal specification of track networks and to generate control tables for specifying the interlocking required between routes. <s> BIB002 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> Ordered Binary-Decision Diagrams (OBDDs) represent Boolean functions as directed acyclic graphs. They form a canonical representation, making testing of functional properties such as satisfiability and equivalence straightforward. A number of operations on Boolean functions can be implemented as graph algorithms on OBDD data structures. Using OBDDs, a wide variety of problems can be solved through symbolic analysis . First, the possible variations in system parameters and operating conditions are encoded with Boolean variables. Then the system is evaluated for all variations by a sequence of OBDD operations. Researchers have thus solved a number of problems in digital-system design, finite-state system analysis, artificial intelligence, and mathematical logic. This paper describes the OBDD data structure and surveys a number of applications that have been solved by OBDD-based symbolic analysis. <s> BIB003 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> This paper describes a formal theory of undirected (labeled) graphs in higher-order logic developed using the mechanical theoremproving system HOL. It formalizes and proves theorems about such notions as the empty graph, single-node graphs, finite graphs, subgraphs, adjacency relations, walks, paths, cycles, bridges, reachability, connectedness, acyclicity, trees, trees oriented with respect to roots, oriented trees viewed as family trees, top-down and bottom-up inductions in a family tree, distributing associative and commutative operations with identities recursively over subtrees of a family tree, and merging disjoint subgraphs of a graph. The main contribution of this work lies in the precise formalization of these graph-theoretic notions and the rigorous derivation of their properties in higher-order logic. This is significant because there is little tradition of formalization in graph theory due to the concreteness of graphs. A companion paper [2] describes the application of this formal graph theory to the mechanical verification of distributed algorithms. <s> BIB004 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <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> BIB005 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> This paper introduces GRASP (Generic seaRch Algorithm for the Satisfiability Problem), an integrated algorithmic framework for SAT that unifies several previously proposed search-pruning techniques and facilitates identification of additional ones. GRASP is premised on the inevitability of conflicts during search and its most distinguishing feature is the augmentation of basic backtracking search with a powerful conflict analysis procedure. Analyzing conflicts to determine their causes enables GRASP to backtrack non-chronologically to earlier levels in the search tree, potentially pruning large portions of the search spare. In addition, by "recording" the causes of conflicts, GRASP can recognize and preempt the occurrence of similar conflicts later on in the search. Finally straightforward bookkeeping of the causality chains leading up to conflicts allows GRASP to identify assignments that are necessary for a solution to be found. Experimental results obtained from a large number of benchmarks, including many from the field of test pattern generation, indicate that application of the proposed conflict analysis techniques to SAT algorithms can be extremely effective for a large number of representative classes of SAT instances. <s> BIB006 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> We take a fresh look at the problem of how to check safety properties of finite state machines. We are particularly interested in checking safety properties with the help of a SAT-solver. We describe some novel induction-based methods, and show how they are related to more standard fixpoint algorithms for invariance checking. We also present preliminary experimental results in the verification of FPGA cores. This demonstrates the practicality of combining a SAT-solver with induction for safety property checking of hardware in a real design flow. <s> BIB007 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> Binary Decision Diagrams (BDDs) have dominated the area of symbolic model checking for the past decade. Recently, the use of satisfiability (SAT) solvers has emerged as an interesting complement to BDDs. SAT-based methods are capable of coping with some of the systems that BDDs are unable to handle.The most challenging problem that has to be solved in order to adapt standard symbolic model checking to SAT-solvers is the boolean quanti fication necessary for traversing the state space. A possible approach to extending the applicability of SAT-based model checkers is therefore to reduce the amount of traversal.In this paper, we investigate a BDD-based verification algorithm due to van Eijk. Van Eijk's algorithm tries to compute information that is sufficient to prove a given safety property directly. When this is not possible, the computed information can be used to reduce the amount of traversal needed by standard model checking algorithms. We convert van Eijk's algorithm to use a SAT-solver instead of BDDs. We also make a number of improvements to the original algorithm, such as combining it with recently developed variants of induction. The result is a collection of substantially strengthened and complete verification methods that do not require state space traversal. <s> BIB008 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> Boolean satisfiability is probably the most studied of the combinatorial optimization/search problems. Significant effort has been devoted to trying to provide practical solutions to this problem for problem instances encountered in a range of applications in electronic design automation (EDA), as well as in artificial intelligence (AI). This study has culminated in the development of several SAT packages, both proprietary and in the public domain (e.g. GRASP, SATO) which find significant use in both research and industry. Most existing complete solvers are variants of the Davis-Putnam (DP) search algorithm. In this paper we describe the development of a new complete solver, Chaff which achieves significant performance gains through careful engineering of all aspects of the search-especially a particularly efficient implementation of Boolean constraint propagation (BCP) and a novel low overhead decision strategy. Chaff has been able to obtain one to two orders of magnitude performance improvement on difficult SAT benchmarks in comparison with other solvers (DP or otherwise), including GRASP and SATO. <s> BIB009 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <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> BIB010 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> Representing BBDs in High Order Logic: <s> We present the verification of the normalization of a binary decision diagram (BDD). The normalization follows the original algorithm presented by Bryant in 1986 and transforms an ordered BDD in a reduced, ordered and shared BDD. The verification is based on Hoare logics and is carried out in the theorem prover Isabelle/HOL. The work is both a case study for verification of procedures on a complex pointer structure, as well as interesting on its own, since it is the first proof of functional correctness of the pointer based normalization process we are aware of. <s> BIB011
BDDs  are data structure used as a compact representation for Boolean functions which improves the capacity of model checkers. Different representations of ROBDDs (Reduced Order Binary Decision Diagrams) BIB003 are used to manipulate the state transition relations as diagrams and this allows model checkers to verify larger systems. Still, most model checkers face the state space explosion problems  . To be able to apply model checking to larger designs, state reduction techniques are used. Examples include partitioned transition relation, dynamic variable reordering, cone of influence reduction, abstraction, problem-specific techniques, e.g. when the original design is rewritten in a simpler way, omitting the irrelevant details, but preserving the important behavior for the property being verified. An alternative for decision graphs is to represent the transition relation by a CNF (Conjunctive Normal Form), then to use SAT BIB001 BIB007 solvers to decide on the satisfiability of these formulae. SAT solvers can decide very large Boolean formulae in reasonable time, but they are not canonical and require additional efforts to check for the equivalence of formulas. As a result, various researchers have developed routines for performing Bounded Model Checking (BMC) BIB008  using SAT. The common theme is to convert the problem of interest into a SAT problem, by devising the appropriate propositional Boolean formula. Then, they exploit the known ability of SAT solvers to find a single satisfying solution when it exists. Moreover, SAT solver technology has improved significantly in recent years with a number of sophisticated packages which are freely available. Well known state-of-the-art SAT solvers include CHAFF BIB009 , GRASP BIB006 and SATO  . Since state sets can be represented as Boolean formulae, and since most model checking techniques manipulate state sets, SAT solvers have enormously boosted their speed and applicability. In high order theorem provers, transition relations are formalized either as DAGs or as terms and formulae. The first is a graphical representation using trees and graphs, while the later is a formal logic representation using datatype. First of all, the graph is represented as a data structure in the theorem prover. This representation should reflect the abstract properties of graphs and should be flexible to be suitable for different domains and for many applications to model complex designs. Several examples can be cited: to model communication networks (railway track network BIB002 ), also in transport industry, the problem of finding the most economical route of delivering goods and the problem of maximizing the network capacity can be solved using graphs. Chou BIB004 gradually formalized a considerable part of graph theory in HOL theorem prover. The theory of undirected graphs is formalized as empty graphs, single-node graphs, finite graphs, subgraphs, paths, reachability, acyclicity, trees, subtrees, and merging disjoint subgraph of a graph. Based on this formalization, the correctness of distributed algorithms has been verified in HOL  . The authors in BIB011 modeled the graph structure of a BDD as heaps then they verified BDDs normalization algorithm in Isabelle/HOL theorem prover. The normalization follows the original algorithm presented by Bryant in 1986 which transforms an ordered BDD into a reduced, ordered and shared BDD. The verification is based on Schirmers research on the Verification Condition Generator (VCG) to generate the proof obligations for Hoare Logic. The authors in  implemented and proved the correctness of BDDs operations completely formalized in Coq. Their objective was to extract certified algorithms for BDDs operations running in Caml (the implementation language of Coq). In their formalization, BDDs were represented as DAGs and the memory in which the BDDs nodes were stored has been formalized as well using pointers such that no new nodes will be created unless necessary. The model was more abstract and the normalization algorithm was not an issue and sharing was simply ignored, since only normalized BDDs will be constructed at all. The main difficulties of the graph formalization is related to data structure sharing and to the side-effects resulted in the computation. The algorithms usually mark the processed nodes or store the results calculated for a subtree or subgraph in a hash-table to avoid recalculation. Moreover, it would be very difficult to get a good performance that it is clearly never expected to compete (in terms of time and space usage) with BDDs libraries written in languages like C. The advantage of course is that there is very little work in this area so probably much scope for research. On the other hand, modeling the transition relations as terms and formulae is smoother for proofs especially those based on induction. Also, in applications like model checking, one would deal with several terms, and any efficient implementation must define sharing. The work presented in  BIB010 [34] BIB005  is an example of this logical approach. The choice between the two approaches depends on the objectives. If we want to reason about the implementation itself and its correctness, then its better to define transition relations as graphs and do sharing of common sub-trees. Clearly this makes the development and proofs complex. On the other hand, if we are only interested in a high-level view of algorithms, then a logical representation is preferred.