Proof Obligations Preserving Compilation Extended abstract

Abstract. The objective of this work is to study the interaction be-tween program verication and program compilation, and to show that the proof that a source program meets its specication can be reused to show that the corresponding compiled program meets the same speci-cation. More concretely, we introduce a core imperative language, and a bytecode language for a stack-based abstract machine, and a non-optimizing compiler. Then we consider for both languages verication condition generators that operate on programs annotated with loop in-variants and procedure specications. In such a setting, we show that compilation preserves proof obligations, in the sense that the proof obli-gations generated for the source annotated program are the same that those generated for the compiled annotated program (using the same loop invariants and procedure specications). Furthermore, we discuss the relevance of our results to Proof Carrying Code.