Model checking guided abstraction and analysis

Abstract

The combination of abstraction and state exploration techniques is the most promising recipe for a successful verification of properties of large or infinite state systems. In this work, we present a general, yet effective, algorithm for computing automatically boolean abstractions of infinite state systems, using decision procedures. The advantage of our approach is that it is not limited to particular concrete domains, but can handle different kinds of infinite state systems. Furthermore, our approach provides, through the use of model checking as a tool for the exploration of the state-space of the abstract system, an automatic way of refining the abstraction until the property of interest is verified or a counterexample is exhibited. We illustrate our approach on some examples and discuss its implementation. © Springer-Verlag Berlin Heidelberg 2000.