A formally verified compiler back-end
From MaRDI portal
Publication:2655327
DOI10.1007/s10817-009-9155-4zbMath1185.68215arXiv0902.2137WikidataQ123335679 ScholiaQ123335679MaRDI QIDQ2655327
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
formal methods; program proof; compiler verification; semantic preservation; compiler transformations and optimizations; the Coq theorem prover
68N20: Theory of compilers and interpreters
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Mechanized Verification of Computing Dominators for Formalizing Compilers, The verified CakeML compiler backend, Cogent: uniqueness types and certifying compilation, Trace-Relating Compiler Correctness and Secure Compilation, A Fast Verified Liveness Analysis in SSA Form, ANF preserves dependent types up to extensional equality, A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler, Trustworthy Graph Algorithms (Invited Talk), Verifying Optimizations for Concurrent Programs, Unnamed Item, Characteristic formulae for liveness properties of non-terminating CakeML programs, Validating safety arguments with Lean, Runtime verification of embedded real-time systems, Impossibility of gathering, a certification, Mechanising a type-safe model of multithreaded Java with a verified compiler, Verified spilling and translation validation with repair, A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data, Non-well-founded deduction for induction and coinduction, Safe functional systems through integrity types and verified assembly, From LCF to Isabelle/HOL, A decision procedure for (co)datatypes in SMT solvers, Automatic refinement to efficient data structures: a comparison of two approaches, A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation, Proof-producing translation of higher-order logic into pure and stateful ML, Programming Inductive Proofs, Relational Decomposition, Animating the Formalised Semantics of a Java-Like Language, Coquet: A Coq Library for Verifying Hardware, Formal Certification of a Resource-Aware Language Implementation, Mining the Archive of Formal Proofs, A Decision Procedure for (Co)datatypes in SMT Solvers
Uses Software
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
