Abstract: Abstraction refinement is one of the most important model checking techniques to alleviate the state explosion problem. The major challenge of an abstraction refinement system is to quickly compute a compact abstract model that preserves the relevant behaviors of the concrete model. This talk presents several algorithms to help achieve this goal.

We describe a new technique, called SAT conflict dependency analysis. For an unsatisfiable CNF formula, this technique can extract the proof of unsatisfiability by analyzing conflict clauses and conflict graphs generated during SAT search. An incremental SAT solver can also be built based on this technique.

Localization reduction is a very simple abstraction technique, yet is very effective for hardware verification. We present two localization reduction algorithms. The first one is based on a syntactic analysis of abstract counterexamples. The other algorithm uses unsatisfiability proofs to identify important registers.

Predicate abstraction can be used to create abstract models that are much smaller than those created by localization reduction. But existing algorithms for predicate abstraction are computationally expensive. We show how to speed up predicate abstraction based on unsatisfiability proofs.

We give experimental results for the verification of industrial hardware designs with up to thousands of registers.