On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> FORMAL VERIFICATION TECHNIQUES <s> 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. <s> BIB001 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> FORMAL VERIFICATION TECHNIQUES <s> 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. <s> BIB002 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> FORMAL VERIFICATION TECHNIQUES <s> 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. <s> BIB003 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> FORMAL VERIFICATION TECHNIQUES <s> 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. <s> BIB004 </s> On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey <s> FORMAL VERIFICATION TECHNIQUES <s> 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. <s> BIB005
Formal verification problem consists of mathematically establishing that an implementation behaves according to a given set of requirements or specification. To classify the various approaches, we first look at three main aspects of the verification process: system under investigation (implementation) set of requirements to obey (specification) and formal verification tool to verify the process (relationship between implementation and specification). Implementation refers to the description of the design that is to be verified. It can be described at different levels of abstraction which results in different verification methods. Another important issue with the implementation is the class of the system or circuit to be verified, i.e., whether it is combinational/sequential, synchronous/asynchronous, pipelined or parameterized hardware. These variations may require different approaches. Specification refers to the property with respect to which the correctness is to be determined. In practice, one needs to model both the implementation and the specification in the logic of the tool, and then uses tool to check the correctness of the system or in some cases give a trace of error (counter-example). Formal verification approaches can be generally divided into two main categories: theorem proving methods and state exploration methods such as model checkers. Theorem Proving is an approach where the specification and the implementation are usually expressed in first-order or higher-order logic. Their relationship is formed as a theorem to be proved within the logic system. The logic is formalized by a set of axioms and a set of inference rules. Steps in the proof appeal to the axioms and rules, and possibly derived definitions and intermediate lemmas. The axioms are usually "elementary" in the sense that they capture the basic properties of the logic's operators BIB003 . Theorem proving utilizes the proof inference technique. The problem itself is transformed into a sequent, a working representation for the theorem proving problem. Then a sequent holds if the formula f holds in any model: A proof system is collection of inference rules of the form: Where C is a conclusion sequent, and i P 's are premises sequent. An inference rule means that if all the premises are derivable then the conclusion is guaranteed to hold. Theorem proving methods have been in use in hardware and software verification for a number of years in various research projects. Some of the wellknown theorem provers are HOL (Higher-Order Logic), ISABELLE, PVS (Prototype Verification System) and Coq BIB003 BIB004 BIB005  . These systems are distinguished by, among other aspects, the underlying mathematical logic, the way automatic decision procedures are integrated into the system, and the user interface. The advantage of the deductive verification approach is that it can handle very complex systems because the logics of theorem provers are more expressive. Even though they are powerful, they require expertise in using a theorem prover. User is expected to know the whole design leading to a white box verification approach. It is not fully automated and requires a large amount of time to verify the system. Another shortcoming is the inability to produce counter-examples in the event of a failed proof, because the user does not know whether the required property is not derivable or whether the person conducting the derivation is not experienced enough with the theorem prover logic. State Exploration Methods use states space traversal algorithms on finite-state models to check if the implementation satisfies its specification. They are focused mostly on automatic decision procedures for solving the verification problem. Model checking is a state exploration based verification technique developed in the 1980s by Clarke and Emerson  and independently by Quielle and Sifakis BIB001 . In model checking, a state of the system under consideration is a snapshot of the system at certain time, given by the set of the variables values of that system at that time. The system is then modeled as a set of states together with a set of transitions between states that describe how the system moves from one state to another in response to internal or external stimulus. Model checking tools are then used to verify that desired properties (expressed in some temporal logic) hold in the system. The state exploration approach has two important advantages. First, once the correct design of the system and the required properties has been fed in, the verification process is fully automatic. Second, in the event of a property not holding, the verification process is able to produce a counter-example (i.e. an instance of the behaviour of the system that violates the property) which is extremely useful in helping the human designers pinpoint and fix the flaw. Model checkers such as SPIN BIB002 , COSPAN  , SMV  , and Multiway Decision Graphs (MDGs)  take as input, essentially, a finite-state system and temporal property in some variety or subset of CTL*, and automatically check that the system satisfies the property. Moreover, the model is often restricted to a finite-state transition system, for which finite-state model checking is known to be decidable. The design or model is formalized in terms of a state machine (Transition System), or a Kripke structure: Where M is a state machine (model) with a transition to describe the circuit behavior, P is a set of atomic propositions, S is a finite set of states, S I ⊆ is a set of initial states, SxS R ⊆ is a transition relation that must be total (i.e. for every Graphs (DAGs), trees and graphs, to save storage space and computation time by eliminating redundancies such as Binary Decision Diagrams (BDDs) and MDGs. 2. Logical representation: As terms and formulae using logic to simplify formulae and benefit of the power of automatic reasoning such as Conjunctive Normal Form (CNF). Model checking is then done by manipulating these formulae using BDDs or SAT solving techniques.