Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification

摘要

In this paper, we develop a counterexample-guided abstrac-tion refinement (CEGAR) framework for monotonic abstraction, an approach that is particularly useful in automatic verification of safety prop-erties for parameterized systems. The main drawback of verification using monotonic abstraction is that it sometimes generates spurious counterex-amples. Our CEGAR algorithm automatically extracts from each spuri-ous counterexample a set of configurations called a "Safety Zone" and uses it to refine the abstract transition system of the next iteration. We have developed a prototype based on this idea; and our experimentation shows that the approach allows to verify many of the examples that cannot be handled by the original monotonic abstraction approach.