Preservation of proof obligations from Java']Java to the Java']Java virtual machine

While program verification environments typically target source programs, there is an increasing need to provide strong guarantees for executable programs. We establish that it is possible to reuse the proof that a source Java program meets its specification to show that the corresponding JVM program, obtained by non-optimizing compilation, meets the same specification. More concretely, we show that verification condition generators for Java and JVM programs generate the same set of proof obligations, when applied to a program p and its compilation [p] respectively. Preservation of proof obligations extends the applicability of Proof Carrying Code, by allowing certificate generation to rely on existing verification technology.