On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey
---
paper_title: Combining theorem proving and trajectory evaluation in an industrial environment

paper_content:

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.
---
paper_title: Introduction to Formal Hardware Verification

paper_content:

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
---
paper_title: An Integration of Model Checking with Automated Proof Checking

paper_content:

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.
---
paper_title: Isabelle: A Generic Theorem Prover

paper_content:

Foundations.- Getting started with Isabelle.- Advanced methods.- Basic use of Isabelle.- Proof management: The subgoal module.- Tactics.- Tacticals.- Theorems and forward proof.- Theories, terms and types.- Defining logics.- Syntax transformations.- Substitution tactics.- Simplification.- The classical reasoner.- Basic concepts.- First-order logic.- Zermelo-Fraenkel set theory.- Higher-order logic.- First-order sequent calculus.- Constructive Type Theory.- Syntax of Isabelle Theories.
---
paper_title: Design And Validation Of Computer Protocols

paper_content:

Part 1 Basic: introduction protocol structure error control flow control. Part 2 Specification and modeling: validation models correctness requirements protocol design finite state machines. Part 3 Conformance testing synthesis and validation: conformance testing protocol synthesis protocol validation. Part 4 Design tools: a protocol simulator a protocol validator using the validator.
---
paper_title: Introduction to HOL: a theorem proving environment for higher order logic

paper_content:

Part I. Tutorial: 1. Introduction to ML 2. The HOL logic 3. Introduction to proof with HOL 4. Goal-oriented proof: tactics and tacticals 5. Example: a simple parity checker 6. How to program a proof tool 7. Example: the binomial theorem Part II. The Meta-Language ML: 8. The history of ML 9. Introduction and examples 10. Syntax of ML 11. Semantics of ML 12. ML types 13. Primitive ML identifier bindings 14. General purpose and list processing functions 15. ML system functions Part III. The Hol Logic: 16. Syntax and semantics 17. Theories Part IV. The Hol System: 18. The HOL logic in ML Part V. Theorem-Proving With HOL: 19. Derived inference rules 20. Conversions 21. Goal-directed proof: tactics and tacticals Appendices.
---
paper_title: A Tutorial Introduction to PVS

paper_content:

This document provides an introductory example, a tutorial, and a compact reference to the PVS veri cation system. It is intended to provide enough information to get you started using PVS, and to help you appreciate the capabilities of the system and the purposes for which it is suitable. Dave Stringer-Calvert provided valuable comments on earlier versions of this tutorial, and also checked the speci cations and proofs appearing here. Preparation of this tutorial was partially funded by NASA Langley Research Center under Contract NAS1-18969, and by the Advanced Research Projects Agency through NASA Ames Research Center NASA-NAG-2-891 (Arpa order A721) to Stanford Unversity.
---
paper_title: Specification and verification of concurrent systems in CESAR

paper_content:

The aim of this paper is to illustrate by an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications.
---
paper_title: Verification of BDD normalization

paper_content:

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.
---
paper_title: A Simple Graph Theory And Its Application In Railway Signaling

paper_content:

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.
---
paper_title: GRASP-A new search algorithm for satisfiability

paper_content:

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.
---
paper_title: SAT-Based Verification without State Space Traversal

paper_content:

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.
---
paper_title: Programming a symbolic model checker in a fully expansive theorem prover

paper_content:

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.
---
paper_title: Checking Safety Properties Using Induction and aSAT-Solver

paper_content:

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.
---
paper_title: A machine program for theorem-proving

paper_content:

The programming of a proof procedure is discussed in connection with trial runs and possible improvements.
---
paper_title: Binary Decision Diagrams as a HOL derived rule

paper_content:

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.
---
paper_title: A Formal Theory of Undirected Graphs in Higher-Order Logic

paper_content:

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.
---
paper_title: Symbolic Boolean manipulation with ordered binary-decision diagrams

paper_content:

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.
---
paper_title: Chaff: Engineering an Efficient SAT Solver

paper_content:

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.
---
paper_title: Combining theorem proving and trajectory evaluation in an industrial environment

paper_content:

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.
---
paper_title: VOSS - A Formal Hardware Verification System User''s Guide

paper_content:

The Voss system is a formal verification system aimed primarily at hardware verification. In particular, verification using symbolic trajectory evaluation is strongly supported. The Voss system consists of a set of programs. The main one is called fl and is the core of the verification system. Since the metalanguage in fl is a fully general functional language in which Ordered Binary Decision Diagrams (OBDDs) have been built in, the verification system is not only useful for carrying out trajectory evaluation, but also for experimenting with various verification (formal and informal) techniques that require the use of OBDDs. This document is intended as both a user''s guide and (to some extent) a reference guide. For the Voss alpha release, this document is still quite incomplete, but work is underway to remedy this.
---
paper_title: PVS: Combining Specification, Proof Checking, and Model Checking

paper_content:

We claim that no single technique such as rewriting, BDDs, or model checking is effective for all aspects of hardware verification. Many examples need the careful integration of these techniques. We have shown some simple examples to illustrate the integration available in PVS. This combination of techniques has been applied to some larger examples such as an SRT divider and Rockwell-Collins AAMP series of processors. The automation available in PVS on these examples can be further improved through the use of more decision procedures (e.g., bit vectors) and better verification methodologies (e.g., abstraction, induction).
---
paper_title: Integrating model checking and theorem proving in a reflective functional language

paper_content:

Forte is a formal verification system developed by Intel's Strategic CAD Labs for applications in hardware design and verification. Forte integrates model checking and theorem proving within a functional programming language, which both serves as an extensible specification language and allows the system to be scripted and customized. The latest version of this language, called reFL ect , has quotation and antiquotation constructs that build and decompose expressions in the language itself. This provides combination of pattern-matching and reflection features tailored especially for the Forte approach to verification. This short paper is an abstract of an invited presentation given at the International Conference on Integrated Formal Methods in 2004, in which the philosophy and architecture of the Forte system are described and an account is given of the role of reFL ect in the system.
---
paper_title: Formal verification of iterative algorithms in microprocessors

paper_content:

Contemporary microprocessors implement many iterative algorithms. For example, the front-end of a microprocessor repeatedly fetches and decodes instructions while updating internal state such as the program counter; floating-point circuits perform divide and square root computations iteratively. Iterative algorithms often have complex implementations because of performance optimizations like result speculation, re-timing and circuit redundancies. Verifying these iterative circuits against high-level specifications requires two steps: reasoning about the algorithm itself and verifying the implementation against the algorithm. In this paper we discuss the verification of four iterative circuits from Intel microprocessor designs. These verifications were performed using Forte, a custom-built verification system; we discuss the Forte features necessary for our approach. Finally, we discuss how we maintained these proofs in the face of evolving design implementations.
---
paper_title: Multiway Decision Graphs for Automated Hardware Verification

paper_content:

Traditional ROBDD-based methods of automated verification suffer from the drawback that they require a binary representation of the circuit. To overcome this limitation we propose a broader class of decision graphs, called {\em Multiway Decision Graphs} (MDGs), of which ROBDDs are a special case. With MDGs, a data value is represented by a single variable of abstract type, rather than by 32 or 64 boolean variables, and a data operation is represented by an uninterpreted function symbol. MDGs are thus much more compact than ROBDDs, and this greatly increases the range of circuits that can be verified. We give algorithms for MDG manipulation, and for implicit state enumeration using MDGs. We have implemented an MDG package and provide experimental results.
---
paper_title: An Integration of Model Checking with Automated Proof Checking

paper_content:

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.
---
paper_title: Certifying Model Checkers

paper_content:

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.
---
paper_title: Programming a symbolic model checker in a fully expansive theorem prover

paper_content:

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.
---
paper_title: Binary Decision Diagrams as a HOL derived rule

paper_content:

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.
---
paper_title: Reachability Programming in HOL98 Using BDDs

paper_content:

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.
---

Title: On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey

Section 1: INTRODUCTION
Description 1: Introduce the complementary approaches of state exploration methods and deductive verification, highlighting strengths, weaknesses, and the motivation for integrating decision diagrams in high-order logic-based theorem provers.

Section 2: FORMAL VERIFICATION TECHNIQUES
Description 2: Discuss the classification of formal verification techniques, focusing on theorem proving methods and state exploration methods such as model checking.

Section 3: Representing BBDs in High Order Logic
Description 3: Explain how Binary Decision Diagrams (BDDs) are represented and manipulated within high-order logic theorem provers.

Section 4: HYBRID APPROACH
Description 4: Review examples and methodologies of integrating proof systems with external automated verification tools, emphasizing high-order logic proof systems.

Section 5: DEEP EMBEDDING APPROACH
Description 5: Detail the concept and implementation of embedding model checking inside theorem provers, focusing on the correctness by construction and the deep embedding of decision graphs.

Section 6: CONCLUSION
Description 6: Summarize the survey findings, stressing the benefits of combining model checking with theorem proving, the challenges of state space explosion, and the future research directions.