Abstract:

Bytecode Model Checking: An Experimental Analysis

David Basin and Stefan Friedrich and Marek Gawkowski and Joachim Posegga


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.