The 2-valued and the 3-Valued Abstraction-Refinement Frameworks in Model Checking

Model checking is a widely used technique for automatic verification of hardware and software systems.  Significant amount of research in model checking is devoted to extending its scope to larger and even infinite-state systems.

Abstraction is one of the most successful approaches for doing so. It hides some of the irrelevant details of the system, thus resulting in a small (abstract) model whose correct behavior can be checked. Sometimes the abstraction is too coarse and a desired property cannot be checked on the abstract model. In this case, the abstract model is refined by adding some of the hidden details back.

In this talk we present two different frameworks for abstraction-refinement in model checking: The 2-valued (CEGAR) and the 3-valued (TVAR) frameworks. We will describe the abstract models and the type of properties that can be verified with those abstractions. We will also show when refinement is needed.