Abstract model checking infinite state systems

Summary form only given. We present an automatic combination of abstraction-refinement by which we translate a model describing an infinite state system to an initial equivalent abstract finite system to explore its state space to verify ctl properties. We present the method implemented to compute automatically abstractions using decision procedures. This method can handle different kinds of infinite state systems including systems composed of concurrent components. Abstract models may admit spurious counterexamples (false negative results) which are executions at the abstract level with no corresponding executions at the concrete level. We devise a new algorithm which analyzes such counterexamples and refine the abstract model correspondingly by eliminating gradually the false negative results. We illustrate our approach on an example and we confirm its effectiveness on a large design.