@Article{	  basin.ea:bytecode:2003,
  abstract	= {Java bytecode verification is traditionally performed by
		  usingdataflow analysis. We investigate an alternative based
		  on reducingbytecode verification to model checking. First,
		  we analyze thecomplexity and scalability of this approach.
		  We show experimentallythat, despite an exponential
		  worst-case time complexity, modelchecking type-correct
		  bytecode using an explicit-state on-the-flymodel checker is
		  feasible in practice, and we give a theoreticalaccount why
		  this is the case. Second, we formalize our approach
		  usingIsabelle/HOL and prove its correctness. In doing so we
		  build on theformalization of the Java Virtual Machine and
		  dataflow analysisframework of Pusch and Nipkow and extend
		  it to a more generalframework for reasoning about
		  model-checking based analysis. Overall,our work constitutes
		  the first comprehensive investigation of thetheory and
		  practice of bytecode verification by model checking.},
  author	= {David Basin and Stefan Friedrich and Marek Gawkowski },
  copyright	= {Kluwer Academic Publishers},
  copyrighturl	= {http://www.wkap.nl/},
  journal	= {Journal of Automated Reasoning},
  language	= {USenglish},
  number	= {3-4},
  pages		= {399--444 },
  pdf		= {papers/2003/bcvjar.pdf},
  title		= {Bytecode Verification by Model Checking},
  volume	= 30,
  year		= 2003
}