Local model checking of Java bytecode

We present a model checking procedure to verify a subset of the Java Virtual Machine Language. The procedure works on a finite tractable state representation of the program: in fact, abstraction techniques are employed, driven by the temporal logic formula representing the property to be checked. A ... View More