A Completely Verified Realistic Bootstrap Compiler

DOI10.1142/S0129054103001947MaRDI QIDQ5696931zbMATH OpenWikidataFDO

Authors Axel Dold, Friedrich W. von Henke, Wolfgang Goerigk

Publication date 19 October 2005

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1142/S0129054103001947

zbMATH Keywords

compiler implementationcompiler verificationimplementation correctnessmechanical theorem provingsoftware verification

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• A formally verified compiler back-end
• scientific article; zbMATH DE number 1956470
• A demonstrably correct compiler
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 1630130
• Verified bytecode verification and type-certifying compilation

Cites work

• Deriving correctness properties of compiled code
• scientific article; zbMATH DE number 108368 (Why is no real title available?)
• Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
• ROPI -- a robust optimization programming interface for C++
• Toward compiler implementation correctness proofs

Cited in

(11)

• scientific article; zbMATH DE number 1630129 (Why is no real title available?)
• scientific article; zbMATH DE number 1630130 (Why is no real title available?)
• Lightweight verification of separate compilation
• Verified software toolchain (invited talk)
• scientific article; zbMATH DE number 1374873 (Why is no real title available?)
• Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
• scientific article; zbMATH DE number 1956470 (Why is no real title available?)
• scientific article; zbMATH DE number 2081101 (Why is no real title available?)
• scientific article; zbMATH DE number 1543049 (Why is no real title available?)
• On Trojan horses of Thompson-Goerigk-type, their generation, intrusion, detection and prevention
• Verified just-in-time compiler on x86

Describes a project that uses

Uses Software

• PVS
• Piton

This page was built for publication: A Completely Verified Realistic Bootstrap Compiler

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