Bytecode model checking: An experimental analysis

Abstract. Java bytecode verification is traditionally performed by a polynomial time dataflow algorithm. We investigate an alternative based on reducing bytecode verification to model checking. Despite an expo-nential 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.