Preservation of proof obligations for hybrid verification methods

Program verification environments increasingly rely on hybrid methods that combine static analyses and verifica-tion condition generation. While such verification environ-ments operate on source programs, it is often preferable to achieve guarantees about executable code. We show that, for a hybrid verification method based on numerical static analysis and verification condition generation, compilation preserves proof obligations and therefore it is possible to transfer evidence from source to compiled programs. Our result relies on the preservation of the solutions of analysis by compilation; this is achieved by relying on a bytecode analysis that performs symbolic execution of stack expres-sions in order to overcome the loss of precision incurred by performing static analyses on compiled (rather than source) code. Finally, we show that hybrid verification methods are sound by proving that every program provable by hy-brid methods is also provable (at a higher cost) by standard methods.