Symbolic transfer function-based approaches to certified compilation

DOI10.1145/964001.964002MaRDI QIDQ3452245zbMATH OpenOpenAlexWikidataFDO

Authors Xavier Rival

Publication date 11 November 2015

Published in Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/964001.964002

zbMATH Keywords

compilationabstract interpretationstatic analysiscertificationtranslation validation

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Certificate Translation for Optimizing Compilers
• scientific article; zbMATH DE number 1953021
• Formal verification of synchronous data-flow program transformations toward certified compilers
• Certifying compilation and run-time code generation
• Computer Aided Verification

Cited in

(8)

• Certificate Translation in Abstract Interpretation
• Inter-program Properties
• A formally verified compiler back-end
• scientific article; zbMATH DE number 1953021 (Why is no real title available?)
• Verifying chemical reaction network implementations: a pathway decomposition approach
• Formal verification of synchronous data-flow program transformations toward certified compilers
• Symbolic computation via program transformation
• Preservation of Proof Obligations from Java to the Java Virtual Machine

This page was built for publication: Symbolic transfer function-based approaches to certified compilation

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