Seminar Abstract

Dr Wolfgang Goerigk
Kiel University

On the Correctness of Compilers and Compiler Implementations

Compiler correctness is crucial to the software engineering of safety critical software. It is well known that in most cases tests are not sufficient to guarantee program correctness. Moreover, it becomes more and more apparent, even in industry, that program verification is needed to meet high reliability requirements for safety critical software. On the other hand, program verification methods are best known to work for semantically clean high level programming languages. However, it is the binary machine code implementation of a program running on a concrete piece of hardware which we ultimately want to trust. Therefore, the language implementation should be proved to carry over program correctness from source to target programs; the compiler has to preserve program correctness. We will discuss different correctness notions for the compiling specification, i.e. for the mapping from source to target programs. Different notions of program correctness give rise to different notions of compiler correctness as well as to different design decisions for code generation.

Of course, the correctness of a compiler itself also depends on both the correctness of its specification and construction as high level program as well as on the correctness of its implementation. Since at present no fully verified compiler for any realistic compiler implementation language is available, at least for the very first time we additionally have to carefully verify the compiler implementation in order to prove compiler correctness as rigorous as required by the correctness of the software development process for safety critical computer based systems. We will describe a specialized bootstrapping technique, using an unverified implementation of the high level compiler implementation language and manually double checking the result to be generated according to the correct specification. A clever choice of intermediate languages will separate crucial compilation steps from each other and modularize the compiler program as well as the manual double checks into smaller parts.

Thursday 5th October


Seminar Room 414, Computer Science, University of Queensland

Last updated: September 28, 1995