@InProceedings{	  psd:2006b,
  author	= {F. Pigorsch and C. Scholl and S. Disch},
  title		= {Advanced Unbounded Model Checking Based on AIGs, BDD
		  Sweeping, And Quantifier Scheduling},
  editor	= {},
  booktitle	= {Proceedings of the Conference on Formal Methods in
		  Computer Aided Design (FMCAD)},
  year		= {2006},
  series	= {},
  volume	= {},
  pages		= {89-96},
  address	= {},
  month		= {Nov},
  organization	= {},
  publisher	= {IEEE Computer Society Press},
  note		= {},
  abstract	= {In this paper we present a complete method for verifying
		  properties expressed in the temporal logic CTL. In contrast
		  to the majority of verification methods presented in recent
		  years, we support unbounded model checking based on
		  symbolic representations of characteristic functions. Among
		  others, our method is based on an advanced And-Inverter
		  Graph (AIG) implementation, quantifier scheduling, and BDD
		  sweeping. For several examples, our method outperforms BDD
		  based symbolic model checking by orders of magnitude.
		  However, our approach is also able to produce competitive
		  results for cases where BDD are known to perform well.},
  copyright	= {IEEE},
  copyrighturl	= {},
  filelabel	= {},
  iranote	= {},
  isbn		= {},
  language	= {USenglish},
  pdf		= {papers/2006/psd2006_fmcad.pdf},
  ps		= {},
  url		= {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4021014}
		  ,
  user		= {}
}