Abstract

Model checking is widely used in the verification of hardware and is gaining acceptance for software as well. Symbolic model checking, in particular, allows the analysis of models with very large numbers of states. Two symbolic approaches are currently in use: One based on fixpoint computations and Binary Decision Diagrams (BDDs), and the other based on bounded computations and satisfiability (SAT) solvers. In this talk we review techniques for model checking invariants, which are the most common type of properties to be verified. We show that many of the approaches proposed to check invariants can be interpreted as strengthening of the invariant until it becomes inductive. We examine BDD-based techniques, and bounded model checking (BMC) techniques, and we discuss the use of abstraction refinement.