A formally verified compiler back-end

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.

References in corpus (1)

• Mechanized semantics for the Clight subset of the C language

Cited by in corpus (36)

• Blockchain Transaction Processing
• Countering Trusting Trust through Diverse Double-Compiling
• Deciding Kleene Algebras in Coq
• Formally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler
• Formal Verification of Hardware Synthesis
• A Survey on Theorem Provers in Formal Methods
• Typed Closure Conversion for the Calculus of Constructions
• Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion
• The Trusted Computing Base of the CompCert Verified Compiler
• Towards Porting Operating Systems with Program Synthesis
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
• Lessons from Formally Verified Deployed Software Systems (Extended version)
• Foundational Extensible Corecursion
• A Framework for Certified Self-Stabilization
• Dynamic Analysis of ARINC 653 RTOS with LLVM
• Robustly Safe Compilation or, Efficient, Provably Secure Compilation
• Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid
• Trustworthy Formal Natural Language Specifications
• Open Transactions on Shared Memory
• Verified type checker for Jolie programming language
• A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
• Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
• Trustworthy Graph Algorithms
• Specifying and Executing Optimizations for Parallel Programs
• Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny
• Memory Simulations, Security and Optimization in a Verified Compiler
• Verified Secure Compilation for Mixed-Sensitivity Concurrent Programs
• Denotation-based Compositional Compiler Verification
• From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
• Formal verification of trading in financial markets
• Embracing a mechanized formalization gap
• A Logical Programming Language as an Instrument for Specifying and Verifying Dynamic Memory
• Pleasant Imperative Program Proofs with GallinaC
• Mechanized semantics
• Verification of the Incremental Merkle Tree Algorithm with Dafny
• From LCF to Isabelle/HOL