Lazy Code Transformations in a Formally Verified Compiler
Léo Gourdin · 2023
Translation validation verifies the results of an untrusted translator—called an oracle—at the compiler’s runtime using a validator. This approach enables validating intricate optimizations without having to prove them directly. Parametrizing such a validator with hints provided by oracles greatly simplifies its integration within a formally verified compiler—such as CompCert. However, generating those hints requires adapting state-of-the-art optimizations.