Java bytecode verification is traditionally performed by a polynomial time data flow algorithm. We investigate an alternative based on reducing bytecode verification to model checking. Despite an exponential worst case time complexity, model checking type-correct bytecode is polynomial in practice when carried out using an explicit state, on the- fly model checker like Spin. We investigate this theoretically and experimentally and explain the practical advantages of this alternative.