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

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

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