Rigorous compiler implementation correctness: How to prove the real thing correct

Abstract

We give a comprehensive technical overview of our work on rigorous verification of compiling specification and compiler implementation of an initial correct binary compiler executable. We will concentrate on implementation verification. Machine program correctness is proved by a special bootstrapping technique with a posteriori code inspection. Our contribution is to perform this work for compilers and, hence, to relieve the application programmer's burden to prove implementation correctness again and again, as this is done today for safety and security critical applications. Once our work has been finished conscientiously and is accepted to reach sufficient mathematical certainty, compilers may be used for proved correct program implementation, safely in the sense that every result a target program execution returns is guaranteed to be correct with respect to the source program semantics.