A formally verified compiler back-end

TL;DR

This paper presents a formally verified compiler back-end from Cminor to PowerPC assembly, ensuring correctness through proof of semantic preservation using Coq, which enhances the reliability of critical software verification.

Contribution

It introduces a verified compiler back-end from Cminor to PowerPC assembly, with correctness proven using Coq, advancing formal methods in software certification.

Findings

Proof of semantic preservation achieved

Compiler correctness verified with Coq

Supports certification of critical software

Abstract

This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.