Verification of Optimizing Compilers

Starting from intermediate representations in static single assignment form, I consider optimizing program transformations and machine code generation. I show how such transformation algorithms can be formally verified. In particular, I address the issue of formalizing these proofs within the Isabelle/HOL system. Furthermore, I discuss the use of program checking to ensure the correctness of the corresponding compiler implementations. Thereby, I introduce a novel checking method which I call "program checking with certificates" and discuss its application to optimizing code generation. In particular, I report on an implementation of this algorithm in a checker for a code generator used in an industrial project. Concludingly, I provide an overview about our further research topics and discuss possibilities to deploy our developed methods also in other areas for the construction of efficient as well as safe and secure systems.