@InProceedings{	  ddhp+:2006,
  author	= {W. Damm and S. Disch and H. Hungar and J. Pang and F.
		  Pigorsch and C. Scholl and U. Waldmann and B. Wirtz},
  title		= {Automatic verification of hybrid systems with large
		  discrete state space},
  editor	= {},
  booktitle	= {Proceedings of the 4th International Symposium on
		  Automated Technology for Verification and Analysis},
  year		= {2006},
  series	= {Lecture Notes in Computer Science},
  volume	= {4218},
  pages		= {},
  address	= {},
  month		= {},
  organization	= {},
  publisher	= {Springer-Verlag},
  note		= {},
  abstract	= {We address the problem of model checking hybrid systems
		  which exhibit nontrivial discrete behavior and thus cannot
		  be treated by considering the discrete states one by one,
		  as most currently available verification tools do. Our
		  procedure relies on a deep integration of several
		  techniques and tools. An extension of And-Inverter-Graphs
		  (AIGs) with first-order constraints serves as a compact
		  representation format for sets of configurations which are
		  composed of continuous regions and discrete states. Boolean
		  reasoning on the AIGs is complemented by first-order
		  reasoning in various forms and on various levels. These
		  include implication checks for simple constraints, test
		  vector generation for fast inequality checks of boolean
		  combinations of constraints, and an exact subsumption check
		  for representations of two configurations. These techniques
		  are integrated within a model checker for universal CTL.
		  Technically, it deals with discrete-time hybrid systems
		  with linear differentials. The paper presents the approach,
		  its prototype implementation, and first experimental
		  data.},
  copyright	= {},
  copyrighturl	= {},
  filelabel	= {},
  iranote	= {},
  isbn		= {},
  language	= {USenglish},
  pdf		= {papers/2006/DDH+_2006.pdf},
  ps		= {},
  public	= {yes},
  url		= {},
  timestamp	= {1168870985},
  user		= {}
}