Abstract. Program verification environments increasingly rely on hybrid methods that combine static analyses and verification condition generation. While such verification environments 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, it is possible to transfer evidence from source to compiled programs. More concretely, we formalize a hybrid verification method for compiled programs and show that compilation preserves proof obligations. The crux of our result is a proof that compilation preserves solutions of analysis; this is achieved by relying on a bytecode analysis that performs symbolic execution of stack expressions in order to overcome the loss of precision incurred by performing static analyses on compiled (rather than source) code. Then, we show that hybrid verification methods are sound by proving that every program provable by hybrid methods is also provable (at a higher cost) by standard methods. Our results generalize to hybrid methods our earlier work on preservation of proof obligations, and warrant their use in Proof Carrying Code scenarios where certificates are generated from source code verification.

[PDF]