On Interpreting Results of Model-Checking with Abstraction
Abstract
Model-checking offers a potential for push-button verification.
Abstraction is often used to combat the state-space explosion problem and
focus the analysis on relevant properties. However, in many such
cases, it is difficult to interpret the results of verification on an
abstract system with respect to a concrete one. In this paper we
present an abstract model-checking approach that guarantees that the
True and False answers are sound with respect to the
original system.