Abstracts FLoC 2010

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. Finally, we will mention some applications of TVAR and try to convince that it is most useful.