Certificate Translation for Optimizing Compilers

DOI10.1007/11823230_20MaRDI QIDQ3613391zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk

Publication date 12 March 2009

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11823230_20

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• Automated Technology for Verification and Analysis
• Securing a compiler transformation
• Securing a compiler transformation
• Certifying compilation and run-time code generation
• Certified compilation for cryptography: extended x86 instructions and constant-time verification
• Reduced Certificates for Abstraction-Carrying Code
• Translation certification for smart contracts

Cited in

(13)

• Certificate Translation in Abstract Interpretation
• A self-certifying compilation framework for WebAssembly
• A formally verified compiler back-end
• Symbolic transfer function-based approaches to certified compilation
• Formal Certification of a Resource-Aware Language Implementation
• Proof optimization for partial redundancy elimination
• Inter-program Properties
• Program and proof optimizations with type systems
• scientific article; zbMATH DE number 2090151 (Why is no real title available?)
• Certifying compilers using higher-order theorem provers as certificate checkers
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• An Introduction to Certificate Translation
• Preservation of Proof Obligations from Java to the Java Virtual Machine

Describes a project that uses

Uses Software

• VLISP

This page was built for publication: Certificate Translation for Optimizing Compilers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3613391)