Local Model Checking of Java Bytecode