Treffer: Java Bytecode Verification Using Model Checking

We provide an abstract interpretation for Java bytecode in order to build finite state models of bytecode programs. The bytecode constraints for assuring safety are formulated in terms of temporal logic formulae. These formulae are checked against the finite program models by a (standard) model checker. By doing so we see a practical way to perform bytecode verification on a formal basis. This could help to achieve higher security and open the door for further extensions to prove additional properties of Java bytecode.