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.