Symbolic transfer function-based approaches to certified compilation

DOI10.1145/964001.964002zbMATH Open1325.68070OpenAlexW2088514859WikidataQ131126900 ScholiaQ131126900MaRDI QIDQ3452245FDOQ3452245

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

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

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)

Cited In (8)

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

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)