@InProceedings{	  basin.ea:verified:2002-b,
  abstract	= {We have used Isabelle/HOL to formalize and prove correct
		  an approach tobytecode verification based on model checking
		  that we have developed forthe Java Virtual Machine. Our
		  work builds on, and extends, theformalization of the Java
		  Virtual Machine and data flow analysisframework of Pusch
		  and Nipkow. By building on their framework, we canreuse
		  their results that relate the run-time behavior of programs
		  withthe existence of well-typings for the programs. Our
		  primary extensionsare to handle polyvariant data flow
		  analysis and its realization astemporal logic model
		  checking. Aside from establishing the correctnessof our
		  model-checking approach, our work contributes to
		  understandingthe interrelationships between classical data
		  flow analysis and programanalysis based on model
		  checking.},
  address	= {Hampton, VA, USA},
  author	= {David Basin and Stefan Friedrich and Marek Gawkowski},
  booktitle	= {Theorem Proving in Higher Order Logics (TPHOLs'02)},
  copyright	= {\copyright Springer-Verlag, Heidelberg},
  editor	= {Victor A. Carre{\~n}o and C{\'e}sar A. Mu{\~n}oz and
		  Sofi{\`e}ne Tahar},
  isbn		= 3540440399,
  language	= {USenglish},
  month		= {August},
  pages		= {47--66},
  pdf		= {papers/2002/0_vbmcs.pdf},
  ps		= {papers/2002/vbmcs.ps.gz},
  publisher	= {Springer-Verlag},
  series	= {LNCS},
  title		= {{V}erified {B}ytecode {M}odel {C}heckers},
  volume	= 2410,
  year		= 2002
}