TVOC: A translation validator for optimizing compilers

DOI10.1007/11513988_29MaRDI QIDQ5716568zbMATH OpenOpenAlexFDO

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

Publication date 10 January 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b138445

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli
• Translation and run-time validation of loop transformations
• Automated Technology for Verification and Analysis
• Formal verification of translation validators
• The code validation tool (CVT). Automatic verification of a compilation process

Cited in

(23)

• TVOC
• Verified spilling and translation validation with repair
• The code validation tool (CVT). Automatic verification of a compilation process
• Automatic validation of code-improving transformations on low-level program representations
• TASS: the toolkit for accurate scientific software
• FEVS: a functional equivalence verification suite for high-performance scientific computing
• A self-certifying compilation framework for WebAssembly
• Product programs and relational program logics
• Formal verification of synchronous data-flow program transformations toward certified compilers
• Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
• A formally verified compiler back-end
• Equality saturation: a new approach to optimization
• Symbolic transfer function-based approaches to certified compilation
• ViDoC - Visual Design of Optimizing Compilers
• Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli
• Automated Technology for Verification and Analysis
• Static Analysis
• Certifying compilers using higher-order theorem provers as certificate checkers
• Software Verification of Hyperproperties Beyond k-Safety
• Predicate abstraction for hyperliveness verification
• Translation and run-time validation of loop transformations
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Relational separation logic

This page was built for publication: TVOC: A translation validator for optimizing compilers

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