Compiler Correctness and Implementation Verification: The Verifix Approach

Compiler correctness is crucial to the software engineeringof safety critical software. It depends onboth the correctness of the compiling specificationand the correctness of the compiler implementation.We will discuss compiler correctness for practicallyrelevant source languages and target machines in orderto find an adequate correctness notion for thecompiling specification, i.e. for the mapping fromsource to target programs with respect to their standardsemantics, which allows for...