I have been working with Lilian Burdy on the definition and the implementation of a framework for Java bytecode program verification.
This involves the definition of a bytecode specification language and a compiler from the high level specification language JML(the Java Modeling Language) to the bytecode specification language.
In order to perform bytecode verification we define a bytecode verification condition generator. The latter is based on a weakest precondition calculus defined for almost all sequential bytecode instructions (except for 64 bytes data and floating point arithmetic). We have both the implementations of the weakest precondition calculus and the JML compiler. They are integrated into the JACK (Java Correctnes Kit ) eclipse plugin.