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.
Most of the work was performed while the first and third authors were working at INRIA.The work was partially supported by
the MOBIUS project.