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.

In this talk, I will briefly present the paper [1] in which 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 solutions of analysis by compilation, that is achieved by relying on a bytecode analysis that performs symbolic execution of stack expressions. Finally, a proof of soundness of hybrid verification methods is shown in the paper.

[1] G. Barthe, C. Kunz, D. Pichardie and J. Samborski-Forlese. Preservation of proof obligations for hybrid verification methods. In SEFM 08. To appear.