@TechReport{	  it:2010-015,
  author	= {Parosh Aziz Abdulla and Yu-Fang Chen and Giorgio Delzanno
		  and Fr{\'e}d{\'e}ric Haziza and Chih-Duo Hong and Ahmed
		  Rezine},
  title		= {Constrained Monotonic Abstraction: a {CEGAR} for
		  Parameterized Verification},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2010},
  number	= {2010-015},
  month		= jun,
  abstract	= {In this paper, we develop a counterexample-guided
		  abstraction refinement (CEGAR) framework for
		  \emph{monotonic abstraction}, an approach that is
		  particularly useful in automatic verification of safety
		  properties for \emph{parameterized systems}. The main
		  drawback of verification using monotonic abstraction is
		  that it sometimes generates spurious counterexamples. Our
		  CEGAR algorithm automatically extracts from each spurious
		  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.}
}