Formal Verification

Chapter 2

Basic formal verification algorithms

In Chapter 2 we describe some of the basic algorithms used to develop practical formal verification tools. We start by reviewing basics of formal logic representations, showing how clever exploitation of symmetry can vastly simplify seemingly complex logic. Building on this, we discuss some concepts of verification and of Boolean algebra. We then introduce BDDs, an important data structure which was responsible for enabling the first generation of industrial-strength model checking tools. After this, we discuss the Satisfiability (SAT) problem, a core challenge of FV which was briefly introduced in the previous chapter. In addition, we provide a brief discussion of model checking concepts and some ...