@InProceedings{   basin.ea:bytecode:2002,
  abstract      = {Java bytecode verification is traditionally performed by a
                  polynomialtime dataflow algorithm. We investigate an
                  alternative based onreducing bytecode verification to model
                  checking. Despite anexponential worst case time complexity,
                  model checking type-correctbytecode is polynomial in
                  practice when carried out using anexplicit state,
                  on-the-fly model checker like SPIN. We investigatethis
                  theoretically and experimentally and explain the practical
                  advantages ofthis alternative.},
  address       = {Grenoble, France},
  author        = {David Basin and Stefan Friedrich and Marek Gawkowski and
                  Joachim Posegga},
  booktitle     = {Model Checking Software, 9th International SPIN Workshop},
  editor        = {Dragan Bosnacki and Stefan Leue},
  isbn          = 3540434771,
  language      = {USenglish},
  month         = {April},
  pages         = {42--59},
  pdf           = {papers/2002/BFGP_spin2002.pdf},
  ps            = {papers/2002/BFGP_spin2002.ps.gz},
  publisher     = {Springer-Verlag},
  series        = {LNCS},
  title         = {{B}ytecode {M}odel {C}hecking: {A}n {E}xperimental
                  {A}nalysis},
  volume        = 2318,
  year          = 2002
}