Translation and run-time validation of loop transformations

DOI10.1007/S10703-005-3402-ZMaRDI QIDQ812060zbMATH OpenOpenAlexFDO

Authors Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, Ying Hu, Lenore D. Zuck

Publication date 23 January 2006

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-005-3402-z

zbMATH Keywords

verification conditionstranslation validationloop transformationsoptimizing compilersglobal optimizationsreordering transformationsrun-time validationspeculative optimizations

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• Computer Aided Verification
• Formal verification of translation validators
• A simple, verified validator for software pipelining
• Automated Technology for Verification and Analysis
• Polycheck: dynamic verification of iteration space transformations on affine programs

Cites work

• scientific article; zbMATH DE number 1953021 (Why is no real title available?)
• scientific article; zbMATH DE number 1798183 (Why is no real title available?)
• scientific article; zbMATH DE number 1903374 (Why is no real title available?)
• scientific article; zbMATH DE number 2102726 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• The code validation tool (CVT). Automatic verification of a compilation process

Cited in

(10)

• scientific article; zbMATH DE number 824665 (Why is no real title available?)
• A self-certifying compilation framework for WebAssembly
• Computer Aided Verification
• Automatic validation of code-improving transformations on low-level program representations
• scientific article; zbMATH DE number 234026 (Why is no real title available?)
• Equality saturation: a new approach to optimization
• Static Analysis
• Verified spilling and translation validation with repair
• Automated Technology for Verification and Analysis
• Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli

Describes a project that uses

Uses Software

• ICS
• CVT
• CVC
• TVOC

This page was built for publication: Translation and run-time validation of loop transformations

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