Practical Construction of Correct Compiler Implementations by Runtime Result Verification

Software verification is an expensive and tedious job, even software in safety critical applications is tested only. This paper deals with the construction of com- pilers as an exmaple for big software systems that are hard to verifiy. We describe how program-checking can be used to establish the full correctness of opti- mizing compilers which may be partly generated by unverified construction tools. We show the practica- bility of our approach with an application to the con- struction of verified optimizing compiler back-ends. The basic idea of program-checking is to use an un- verified algorithm whose results are checked by a ver- ified component at run time. Run-Time Result Veri- fication in our approach assures formal correctness of the compilation process and its implementation. In our example the approach does not only simplify the construction of verified compilers because checking the result of the transformations is much simpler to verify than the verification of an optimizing code se- lection. Furthermore, we are still able to use existing compiler generator tools without modifications. This work points out the tasks which still have to be ver- ified and it discusses the flexibility of the approach. 1