Formal verification of translation validators

DOI10.1145/1328438.1328444MaRDI QIDQ3189822zbMATH OpenOpenAlexFDO

Authors Jean-Baptiste Tristan, Xavier Leroy

Publication date 12 September 2014

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

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

zbMATH Keywords

scheduling optimizationsthe Coq proof assistanttranslation validationverified compilers

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A Framework for Formal Verification of Compiler Optimizations
• Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 1670784
• Formal verification of synchronous data-flow program transformations toward certified compilers
• scientific article; zbMATH DE number 1796127

Cited in

(17)

• Verified spilling and translation validation with repair
• Automatic validation of code-improving transformations on low-level program representations
• Formal verification of synchronous data-flow program transformations toward certified compilers
• A formally verified compiler back-end
• scientific article; zbMATH DE number 1670745 (Why is no real title available?)
• scientific article; zbMATH DE number 1696505 (Why is no real title available?)
• Formal validation of pattern matching code
• Trustworthy variant derivation with translation validation for safety critical product lines
• scientific article; zbMATH DE number 1857501 (Why is no real title available?)
• Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli
• Automated Technology for Verification and Analysis
• Computer Aided Verification
• Certifying compilers using higher-order theorem provers as certificate checkers
• Relational bytecode correlations
• Translation and run-time validation of loop transformations
• Automatic generation and validation of instruction encoders and decoders
• A verified framework for higher-order uncurrying optimizations

Describes a project that uses

Uses Software

• Coq
• TVOC
• CVT

This page was built for publication: Formal verification of translation validators

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