- Black-Box Equivalence Checking Across Compiler Optimizations
- Modeling undefined behaviour semantics for checking equivalence across compiler optimizations
- Evaluating value-graph translation validation for LLVM
- Formally Verified Compilation of Low-Level C code
- Proving the correctness of heuristically optimized code
- Semantic Program Alignment for Equivalence Checking
- Translation validation
- TACAS 1998
- Amir Pnueli, Michael Siegel, Eli Singerman
- https://dl.acm.org/citation.cfm?id=349314
- "We present the notion of translation validation as a new approach to the verification of translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verification), each individual translation (i.e. a run of the compiler) is followed by a validation phase which verifies that the target code produced on this run correctly implements the submitted source program."
- Translation Validation: Automatically Proving the Correctness of Translations Involving Optimized Code
- Translation Validation: From DC+ to C*
- FM-Trends 1998
- Amir Pnueli, Ofer Shtrichman, Michael Siegel
- https://dl.acm.org/citation.cfm?id=729871
- "Translation validation is an alternative to the verification of translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verification), each individual translation (i.e. a run of the compiler) is followed by a validation phase which verifies that the target code produced on this run correctly implements the submitted source program."
- Translation validation for an optimizing compiler
- Translation Validation for Verified, Efficient and Timely Operating Systems
- Translation Validation of Bounded Exhaustive Test Cases
- Validating Optimizations of Concurrent C/C++ Programs
Tags:
language development
Last modified 26 February 2026