An Architecture for Verified Compiler Construction

Verified compilers are essential for the development of safetycriticalsoftware systems. Critical parts of control systems are still oftenwritten and verified at the assembler level, because compilers forhigh-level languages are not considered trustworthy. For industrial applications,the techniques for the construction of correct compilers mustbe easy to apply and must be integrated in the software developmentprocess. This raises not only verification problems at the algorithmic...