A formally verified compiler back-end

DOI10.1007/s10817-009-9155-4zbMath1185.68215arXiv0902.2137OpenAlexW2148662736WikidataQ123335679 ScholiaQ123335679MaRDI QIDQ2655327

Xavier Leroy

Publication date: 25 January 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0902.2137

zbMATH Keywords

formal methodsprogram proofcompiler verificationsemantic preservationcompiler transformations and optimizationsthe Coq theorem prover

Mathematics Subject Classification ID

Related Items (31)

A decision procedure for (co)datatypes in SMT solvers ⋮ Trace-Relating Compiler Correctness and Secure Compilation ⋮ A Fast Verified Liveness Analysis in SSA Form ⋮ ANF preserves dependent types up to extensional equality ⋮ Mining the Archive of Formal Proofs ⋮ A Decision Procedure for (Co)datatypes in SMT Solvers ⋮ A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler ⋮ Formal Certification of a Resource-Aware Language Implementation ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Validating safety arguments with Lean ⋮ Verified spilling and translation validation with repair ⋮ Unnamed Item ⋮ A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation ⋮ Verifying Optimizations for Concurrent Programs ⋮ Safe functional systems through integrity types and verified assembly ⋮ Runtime verification of embedded real-time systems ⋮ Impossibility of gathering, a certification ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data ⋮ Mechanized Verification of Computing Dominators for Formalizing Compilers ⋮ Programming Inductive Proofs ⋮ From LCF to Isabelle/HOL ⋮ The verified CakeML compiler backend ⋮ Relational Decomposition ⋮ Animating the Formalised Semantics of a Java-Like Language ⋮ Non-well-founded deduction for induction and coinduction ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ Coquet: A Coq Library for Verifying Hardware ⋮ Cogent: uniqueness types and certifying compilation ⋮ Proof-producing translation of higher-order logic into pure and stateful ML

Uses Software

• Coq
• veriSoft
• TVOC
• VLISP
• CompCert
• cminor
• CIL
• Piton
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Resources, concurrency, and local reasoning
• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Coinductive big-step operational semantics
• Java bytecode verification: Algorithms and formalizations
• Extracting a data flow analyser in constructive logic
• Mechanized semantics for the clight subset of the C language
• Stack-based typed assembly language
• Biorthogonality, step-indexing and compiler correctness
• Formal verification of translation validators
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Symbolic transfer function-based approaches to certified compilation
• Extraction in Coq: An Overview
• Separation Logic for Small-Step cminor
• Compilation as Rewriting in Higher Order Logic
• Certificate Translation for Optimizing Compilers
• Toward compiler implementation correctness proofs
• The Zipper
• Stack-based typed assembly language
• Oracle-based checking of untrusted software
• Proving correctness of compiler optimizations by temporal logic
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Formal certification of a compiler back-end or
• Oracle Semantics for Concurrent Separation Logic
• Certificate Translation in Abstract Interpretation
• Static Analysis
• Computer Aided Verification
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
• Types for Proofs and Programs
• Types for Proofs and Programs

This page was built for publication: A formally verified compiler back-end