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
• Formal verification of VLIW microprocessors with speculative execution
• Formal verification of synchronous data-flow program transformations toward certified compilers
• Transformation-based verification using generalized retiming

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
• Verified optimization for the Intel IA-64 architecture
• A system for object code validation
• Formal validation of pattern matching code
• Trustworthy variant derivation with translation validation for safety critical product lines
• Verification of basic block schedules using RTL transformations
• 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

• CVT
• Coq
• TVOC

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)